aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTLib2Interface.cpp
Commit message (Expand)AuthorAgeFilesLines
* Display better error message in SMTLib2Leonardo Alt2018-11-231-4/+4
* Inject SMTLIB2 queries and responses via standard-json-io.chriseth2018-11-231-9/+12
* [SMTChecker] Add ArraySort and array operationsLeonardo Alt2018-11-221-0/+5
* [SMTChecker] Add FunctionSort and refactors the solver interface to create va...Leonardo Alt2018-11-221-29/+31
* 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-9/+9
* [SMTChecker] Implement uninterpreted functions and use it for blockhash()Leonardo Alt2018-11-151-2/+18
* [SMTLib2] Fix repeated declarationsLeonardo Alt2018-07-281-11/+26
* Fix unterminated parentheses typo in SMTLib2Alex Beregszaszi2018-07-281-1/+1
* [SMTChecker] SMTPortfolio: use all SMT solvers availableLeonardo Alt2018-07-271-6/+3
* Only ask for a model if it's SATLeonardo Alt2018-07-271-1/+1
* Introduce sorts for smt expressions.chriseth2017-11-221-9/+2
* SMT enforce variable typesAlex Beregszaszi2017-10-051-1/+8
* Review changes.chriseth2017-08-231-3/+3
* Refactor Z3 read callback.chriseth2017-08-231-1/+13
* Rename read file callback.chriseth2017-08-231-2/+4
* Insert abstraction layer.chriseth2017-08-231-5/+16
* Cleanup.chriseth2017-08-231-126/+42
* Use file to communicate with z3.chriseth2017-08-231-0/+222
* Rewrite using SMTLIB2 interface.chriseth2017-08-231-0/+24