Christian Parpart
|
6b23412fae
|
C++ namespace cleanup (except tests).
|
2020-01-07 15:51:50 +01:00 |
|
Leonardo Alt
|
67d82fc8a7
|
[SMTChecker] Use rlimit instead of tlimit for SMT queries
|
2019-12-04 11:52:18 +01:00 |
|
Leonardo Alt
|
6b10efff8c
|
Add CHCSmtLib2Interface
|
2019-11-07 11:12:11 +01:00 |
|
Leonardo Alt
|
71144d0d39
|
[CHCChecker] Add CHCSolverInterface and Z3CHCSolverInterface
|
2019-07-15 17:31:39 +02:00 |
|
Leonardo Alt
|
cce377833a
|
Sort includes in libsolidity/formal
|
2018-12-17 18:26:10 +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 |
|
Leonardo Alt
|
87a38e1abe
|
[SMTChecker] SMTPortfolio: use all SMT solvers available
|
2018-07-27 16:15:34 +01:00 |
|
Leonardo Alt
|
ae3350ae03
|
[SMTChecker] Integration with CVC4
|
2018-04-17 12:26:58 +01:00 |
|
chriseth
|
ab5e3a8f6d
|
Introduce native Z3 support.
|
2017-08-23 17:37:35 +02:00 |
|