18 Commits

Author	SHA1	Message	Date
Leonardo Alt	41ac3d6cfb	Remove repeated declarations in Z3 and CVC4 as well	2018-08-01 11:12:56 +02:00
Leonardo Alt	87a38e1abe	[SMTChecker] SMTPortfolio: use all SMT solvers available	2018-07-27 16:15:34 +01:00
Leonardo Alt	b356f6a7f9	Setting timeout to Z3 and CVC4	2018-07-27 16:01:48 +02:00
Leonardo Alt	06dbcb3afe	Only ask for a model if it's SAT	2018-07-27 14:13:22 +02:00
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