Commit Graph
14 Commits
Author SHA1 Message Date
Leonardo Alt ae3350ae03 [SMTChecker] Integration with CVC4 2018-04-17 12:26:58 +01:00
Leonardo Alt 5d74b862a3 This z3 option is necessary for good solving performance 2018-03-04 14:42:36 +01:00
chriseth 19e067465a Unary operators and division. 2017-11-30 01:20:21 +01:00
chriseth 95a65dc04c Fix boolean constants. 2017-11-22 02:35:34 +00:00
chriseth 22c689d516 Check for conditions being constant. 2017-11-22 02:35:34 +00:00
Alex Beregszaszi 7a4c165518 Remove unused variable in Z3 2017-10-18 23:18:11 +01:00
chriseth 153ae98878 Catch exception in Z3.
Note: This exception might not be the result of resource limitation,
it might also hint towards usage error.
2017-10-17 18:30:10 +01:00
Alex Beregszaszi a71c6faf0f Remove duplicate >= in Z3 2017-10-17 18:30:07 +01:00
Alex Beregszaszi 66b188cce9 Merge pull request #3022 from ethereum/assert
Use solAssert and not assert
2017-10-04 14:11:43 +01:00
Alex Beregszaszi a9847c9551 Use solAssert and not assert 2017-10-04 13:05:55 +01:00
chriseth 5ee3ceaef7 Remove leftover couts. 2017-09-29 12:44:39 +02:00
chriseth cf5e1d6120 Review changes. 2017-08-23 17:37:35 +02:00
chriseth 75f09f2a84 Partial support for if statements. 2017-08-23 17:37:35 +02:00
chriseth ab5e3a8f6d Introduce native Z3 support. 2017-08-23 17:37:35 +02:00