aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SolverInterface.h
Commit message (Expand)AuthorAgeFilesLines
* Sort includes in libsolidity/formalLeonardo Alt2018-12-181-4/+2
* [SMTChecker] Support to mappingLeonardo Alt2018-12-141-3/+12
* [SMTChecker] Make smt::Sort::operator== virtualLeonardo Alt2018-11-301-6/+16
* Fix move bug.chriseth2018-11-291-1/+2
* Inject SMTLIB2 queries and responses via standard-json-io.chriseth2018-11-231-0/+3
* Stylechriseth2018-11-231-7/+9
* [SMTChecker] Add ArraySort and array operationsLeonardo Alt2018-11-221-2/+49
* [SMTChecker] Add FunctionSort and refactors the solver interface to create va...Leonardo Alt2018-11-221-21/+29
* 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-60/+48
* [SMTChecker] Implement uninterpreted functions and use it for blockhash()Leonardo Alt2018-11-151-13/+14
* Retained move/copy semantics; removed const qualifier from Expression's membe...Bhargava Shastry2018-10-171-2/+4
* Fix compiler warning: clang-8 warns of explicitly-defined op implicitly delet...Bhargava Shastry2018-10-171-2/+0
* [SMTChecker] Add CheckResult::CONFLICTINGLeonardo Alt2018-07-271-1/+1
* [SMTChecker] SMTPortfolio: use all SMT solvers availableLeonardo Alt2018-07-271-3/+9
* Setting timeout to Z3 and CVC4Leonardo Alt2018-07-271-1/+4
* Add virtual destructors on base classes.Alexander Arlt2018-05-021-0/+1
* [SMTChecker] Integration with CVC4Leonardo Alt2018-04-171-0/+20
* [SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests.Leonardo Alt2018-03-131-6/+23
* [SMTChecker] Support to Bool variablesLeonardo Alt2018-03-131-5/+10
* [SMTChecker] Keep track of current path conditionsLeonardo Alt2017-12-141-0/+5
* Unary operators and division.chriseth2017-11-301-0/+4
* Explain IntIntFun and merge assertion.chriseth2017-11-241-3/+7
* Introduce sorts for smt expressions.chriseth2017-11-221-31/+35
* Check for conditions being constant.chriseth2017-11-221-0/+1
* Remove parameter names for defaulted functions.chriseth2017-08-311-4/+4
* Review changes.chriseth2017-08-231-1/+1
* Partial support for if statements.chriseth2017-08-231-0/+7
* Refactor Z3 read callback.chriseth2017-08-231-2/+5
* Insert abstraction layer.chriseth2017-08-231-0/+168