aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTLib2Interface.h
Commit message (Collapse)AuthorAgeFilesLines
* Sort includes in libsolidity/formalLeonardo Alt2018-12-181-7/+4
|
* Display better error message in SMTLib2Leonardo Alt2018-11-231-2/+2
|
* Inject SMTLIB2 queries and responses via standard-json-io.chriseth2018-11-231-2/+8
|
* [SMTChecker] Add FunctionSort and refactors the solver interface to create ↵Leonardo Alt2018-11-221-5/+5
| | | | variables
* Isolating files shared between Yul- and Solidity language frontend.Christian Parpart2018-11-221-1/+1
|
* [SMTChecker] Refactor smt::Sort and its usageLeonardo Alt2018-11-211-2/+2
|
* [SMTChecker] Implement uninterpreted functions and use it for blockhash()Leonardo Alt2018-11-151-1/+2
|
* [SMTLib2] Fix repeated declarationsLeonardo Alt2018-07-281-0/+3
|
* [SMTChecker] SMTPortfolio: use all SMT solvers availableLeonardo Alt2018-07-271-3/+3
|
* Introduce sorts for smt expressions.chriseth2017-11-221-8/+0
|
* SMT enforce variable typesAlex Beregszaszi2017-10-051-0/+8
|
* Mark constructors explicitAlex Beregszaszi2017-09-201-1/+1
|
* Refactor Z3 read callback.chriseth2017-08-231-2/+4
|
* Rename read file callback.chriseth2017-08-231-1/+1
|
* Insert abstraction layer.chriseth2017-08-231-115/+12
|
* Cleanup.chriseth2017-08-231-13/+16
|
* Use file to communicate with z3.chriseth2017-08-231-6/+29
|
* Rewrite using SMTLIB2 interface.chriseth2017-08-231-0/+150