cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Decrease rlimit

Browse Source
This commit is contained in:
Leonardo Alt 2020-09-23 19:28:47 +02:00
parent 27f768f4d6
commit ebb6f61506
6 changed files with 9 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsmtutil/Z3Interface.h
View File

@ -49,7 +49,7 @@ public:
// Z3 "basic resources" limit.
// This is used to make the runs more deterministic and platform/machine independent.
static int const resourceLimit = 12500000;
static int const resourceLimit = 1000000;
private:
void declareFunction(std::string const& _name, Sort const& _sort);

2
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
View File

@ -22,5 +22,7 @@ contract LoopFor2 {
}
// ----
// Warning 1218: (229-234): Error trying to invoke SMT solver.
// Warning 1218: (296-316): Error trying to invoke SMT solver.
// Warning 6328: (320-339): Assertion violation happens here.
// Warning 6328: (343-362): Assertion violation happens here.
// Warning 4661: (296-316): Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
View File

@ -9,3 +9,4 @@ contract C {
}
}
// ----
// Warning 1218: (174-212): Error trying to invoke SMT solver.

1
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
View File

@ -9,3 +9,4 @@ contract C {
}
}
// ----
// Warning 1218: (166-183): Error trying to invoke SMT solver.

3
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
View File

@ -11,4 +11,5 @@ contract C {
}
}
// ----
// Warning 6328: (173-192): Assertion violation happens here.
// Warning 1218: (173-192): Error trying to invoke SMT solver.
// Warning 7812: (173-192): Assertion violation might happen here.

2
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
View File

@ -10,3 +10,5 @@ contract C {
}
}
// ----
// Warning 1218: (157-172): Error trying to invoke SMT solver.
// Warning 7812: (157-172): Assertion violation might happen here.