12 Commits

Author	SHA1	Message	Date
Leonardo Alt	9a33367bc6	[SMTChecker] Warn when no solver was found and there are unhandled queries.	2019-01-29 14:29:07 +01:00
Leonardo Alt	6251a289dd	Testing with smtlib2 interface always there	2018-11-23 09:43:49 +01:00
Leonardo Alt	dee0c4ded8	Error message stays in the SMTChecker	2018-11-23 09:43:49 +01:00
Leonardo Alt	f3c2309c73	Display better error message in SMTLib2	2018-11-23 09:43:49 +01:00
chriseth	54bed454f6	Rename function and warn if responses are supplied for Z3.	2018-11-23 09:43:49 +01:00
chriseth	bb10be789c	Inject SMTLIB2 queries and responses via standard-json-io.	2018-11-23 09:43:49 +01:00
Leonardo Alt	13a142b039	[SMTChecker] Add FunctionSort and refactors the solver interface to create variables	2018-11-22 10:04:04 +01: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
Alex Beregszaszi	179427fd65	Import dev::solidity namespace in SMTPortfolio	2018-07-27 23:17:17 +01:00
Leonardo Alt	55c1fb60b4	[SMTChecker] Add CheckResult::CONFLICTING	2018-07-27 16:16:26 +01:00
Leonardo Alt	87a38e1abe	[SMTChecker] SMTPortfolio: use all SMT solvers available	2018-07-27 16:15:34 +01:00