aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTChecker.cpp
Commit message (Expand)AuthorAgeFilesLines
* Supported types listed in SSAVariableLeonardo Alt2018-03-011-2/+2
* Integer min and max values placed under SymbolicIntVar instead of SMTCheckerLeonardo Alt2018-03-011-11/+3
* [SMTChecker] A little refactoring on SSA varsLeonardo Alt2018-03-011-46/+35
* [SMTChecker] Variables are merged after branches (ite variables)Leonardo Alt2018-01-051-7/+25
* [SMTChecker] Fix typo in the code (satisifable->satisfiable)Leonardo Alt2017-12-191-6/+6
* [SMTChecker] Helper functions to add an expression to the solver conjoined wi...Leonardo Alt2017-12-141-5/+15
* [SMTChecker] Keep track of current path conditionsLeonardo Alt2017-12-141-8/+27
* Fix expression creation problems.chriseth2017-11-301-19/+30
* Fix signed division.chriseth2017-11-301-2/+16
* Unary operators and division.chriseth2017-11-301-56/+135
* Fix problem with non-value-typed variables.chriseth2017-11-221-13/+13
* For loop.chriseth2017-11-221-0/+42
* Check for conditions being constant.chriseth2017-11-221-26/+87
* Tests.chriseth2017-11-221-5/+0
* Track usage of variables.chriseth2017-11-221-62/+68
* Handle branches.chriseth2017-11-221-54/+78
* Rename variables in SMT checker.chriseth2017-10-181-9/+9
* SMT should not crash on typecast/structsAlex Beregszaszi2017-10-051-0/+10
* Review changes.chriseth2017-08-231-11/+11
* Use experimental feature pragma for SMT checker.chriseth2017-08-231-6/+1
* Partial support for if statements.chriseth2017-08-231-15/+94
* Format numbers more nicely.chriseth2017-08-231-11/+25
* Refactor Z3 read callback.chriseth2017-08-231-3/+24
* Insert abstraction layer.chriseth2017-08-231-26/+27
* Prepare build system for Z3.chriseth2017-08-231-0/+3
* Cleanup.chriseth2017-08-231-4/+443
* z3 conditionschriseth2017-08-231-0/+36