aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTChecker.cpp
Commit message (Expand)AuthorAgeFilesLines
* [SMTChecker] Declaring all state vars before any function is visitedLeonardo Alt2018-05-151-2/+13
* [SMTChecker] Support to integer and Bool storage varsLeonardo Alt2018-05-151-4/+29
* Revert "BREAKING: Bool variables should not allow arithmetic comparison"chriseth2018-05-021-1/+5
* Bool variables should not allow arithmetic comparisonLeonardo Alt2018-04-271-5/+1
* [SMTChecker] Remove 'information is erase' message for if-elseLeonardo Alt2018-04-191-9/+9
* [SMTChecker] Using solUnimplementedAssert instead of solAssert when applicableLeonardo Alt2018-04-181-2/+2
* [SMTChecker] Integration with CVC4Leonardo Alt2018-04-171-0/+4
* [SMTChecker_Bool] Fix PR review comments: method renaming and solAssertLeonardo Alt2018-03-131-7/+8
* [SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests.Leonardo Alt2018-03-131-16/+32
* [SMTChecker] Support to Bool variablesLeonardo Alt2018-03-131-1/+1
* 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 12:44:30 +0800