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

Merge pull request #9873 from ethereum/smt_dec_rlimit

Browse Source 
[SMTChecker] Decrease rlimit
This commit is contained in:
Leonardo 2020-09-23 23:11:59 +02:00 committed by GitHub
commit 35a7d5d3e4
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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.