19 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
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
Alex Beregszaszi	a5a61a0b77	More consistent catch statements ... Also take const& in all cases.	2018-07-25 01:18:09 +01:00
Leonardo Alt	ae3350ae03	[SMTChecker] Integration with CVC4	2018-04-17 12:26:58 +01:00