aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTLib2Interface.cpp
Commit message (Collapse)AuthorAgeFilesLines
* [SMTChecker] Add ArraySort and array operationsLeonardo Alt2018-11-221-0/+5
|
* [SMTChecker] Add FunctionSort and refactors the solver interface to create ↵Leonardo Alt2018-11-221-29/+31
| | | | 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-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
| | | | Found by @leonardoalt
* [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