aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/Z3Interface.cpp
Commit message (Expand)AuthorAgeFilesLines
* Sort includes in libsolidity/formalLeonardo Alt2018-12-181-1/+0
* [SMTChecker] Add ArraySort and array operationsLeonardo Alt2018-11-221-0/+9
* [SMTChecker] Add FunctionSort and refactors the solver interface to create va...Leonardo Alt2018-11-221-12/+12
* 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-7/+7
* [SMTChecker] Implement uninterpreted functions and use it for blockhash()Leonardo Alt2018-11-151-1/+9
* Removing extra default cases to force compile time error, instead of runtime.Anurag Dashputre2018-09-301-2/+0
* Remove repeated declarations in Z3 and CVC4 as wellLeonardo Alt2018-08-011-3/+6
* [SMTChecker] SMTPortfolio: use all SMT solvers availableLeonardo Alt2018-07-271-6/+3
* Setting timeout to Z3 and CVC4Leonardo Alt2018-07-271-0/+3
* Only ask for a model if it's SATLeonardo Alt2018-07-271-1/+1
* [SMTChecker] Integration with CVC4Leonardo Alt2018-04-171-16/+1
* This z3 option is necessary for good solving performanceLeonardo Alt2018-03-041-0/+1
* Unary operators and division.chriseth2017-11-301-1/+4
* Fix boolean constants.chriseth2017-11-221-2/+7
* Check for conditions being constant.chriseth2017-11-221-1/+1
* Remove unused variable in Z3Alex Beregszaszi2017-10-191-1/+1
* Catch exception in Z3.chriseth2017-10-181-18/+27
* Remove duplicate >= in Z3Alex Beregszaszi2017-10-181-2/+1
* Merge pull request #3022 from ethereum/assertAlex Beregszaszi2017-10-041-1/+1
|\
| * Use solAssert and not assertAlex Beregszaszi2017-10-041-1/+1
* | Remove leftover couts.chriseth2017-09-291-7/+0
|/
* Review changes.chriseth2017-08-231-3/+3
* Partial support for if statements.chriseth2017-08-231-1/+11
* Introduce native Z3 support.chriseth2017-08-231-0/+179
generated by cgit (git 2.34.1) at 2024-11-18 01:15:11 +0800