32 Commits

Author	SHA1	Message	Date
Leonardo Alt	6b10efff8c	Add CHCSmtLib2Interface	2019-11-07 11:12:11 +01:00
Leonardo Alt	10e70b8603	[SMTChecker] Support inheritance and resolve overrides	2019-11-06 11:00:06 +01:00
Leonardo Alt	a774b2d905	[SMTChecker] Zero-initialize arrays	2019-09-02 22:37:30 +02:00
Leonardo Alt	1221eeebf1	[SMTChecker] Report malformed expressions more precisely	2019-06-06 11:54:29 +02:00
Leonardo Alt	f281c94b42	[SMTChecker] Test that non-Boolean literals are actually integers	2019-06-05 10:51:05 +02:00
Leonardo Alt	d9ce9cab99	[SMTChecker] Use smtlib's implies instead of \!a or b	2019-06-04 14:23:44 +02:00
Leonardo Alt	637546850f	[SMTChecker] Add mod operator	2019-02-07 14:24:40 +01:00
Leonardo Alt	cce377833a	Sort includes in libsolidity/formal	2018-12-17 18:26:10 +01:00
Leonardo Alt	20accf1a90	[SMTChecker] Add ArraySort and array operations	2018-11-22 14:04:20 +01:00
Leonardo Alt	13a142b039	[SMTChecker] Add FunctionSort and refactors the solver interface to create variables	2018-11-22 10:04:04 +01:00
Christian Parpart	87821c53c3	Isolating files shared between Yul- and Solidity language frontend.	2018-11-21 18:58:12 +00:00
Leonardo Alt	01ce43e51b	[SMTChecker] Refactor smt::Sort and its usage	2018-11-21 15:46:47 +01:00
Leonardo Alt	70bb0eaf95	[SMTChecker] Implement uninterpreted functions and use it for blockhash()	2018-11-15 09:12:42 +01:00
Anurag Dashputre	3321000f67	Removing extra default cases to force compile time error, instead of runtime.	2018-09-30 12:40:38 +05:30
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