Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Boogie: added type 'real' with overloaded arithmetic operations plus real ↵ | boehmes | 2012-09-27 |
| | | | | | | | | | division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested) | ||
* | added floating point keywords to reserved SMTwords list | qadeer | 2012-02-20 |
| | |||
* | SMTLib: Only use (set-logic ...) when requested; quote some more symbols | Michal Moskal | 2011-06-30 |
| | |||
* | Replaced all dictionaries that mapped to bool (i.e., were being used to ↵ | mikebarnett | 2011-03-10 |
| | | | | implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null. | ||
* | Add MULTI_TRACES prover option (equivalent of /z3multipleErrors) | MichalMoskal | 2011-02-23 |
| | |||
* | Remove workaround for Z3 scanner problems (fixed now); fix one comment | MichalMoskal | 2011-02-18 |
| | |||
* | Handle bitvectors | MichalMoskal | 2011-02-18 |
| | |||
* | Use explicit mechanism for skipping to the next assertion | MichalMoskal | 2011-02-17 |
| | |||
* | Fix printing of type-proxies | MichalMoskal | 2011-02-16 |
| | |||
* | Workaround bug in Z3 SMT parser | MichalMoskal | 2011-02-15 |
| | |||
* | Use SMT2 top-level syntax | MichalMoskal | 2011-02-15 |
| | |||
* | Print terms in SMT2 syntax (drop term/formula distinction) | MichalMoskal | 2011-02-15 |
| | |||
* | Move name-quoting (already for SMT2 not SMT1) into a seprate class | MichalMoskal | 2011-02-15 |