Commit Graph

8 Commits

Author SHA1 Message Date
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