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 |
|