| Commit message (Collapse) | Author | Age |
| |
|
| |
|
| |
|
|
|
|
|
|
| |
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
|
|
|
|
|
|
|
|
|
| |
./AbsHoudini/
./doomed/
./z3api/
./test17/
because their conversion to lit incomplete.
|
|
|
|
| |
spaces.
|
| |
|
| |
|
|
|
|
| |
Bizarely Array.bpl does not pass on Windows. This will be fixed soon.
|
| |
|
|
|
|
| |
enabled it to be always on
|
|
|
|
| |
many of the test suite dirs
|
| |
|
|
|
|
| |
temporary hack in FloydCycleDetect.dfy to be corrected shortly)
|
|
|
|
|
|
|
|
|
| |
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)
|
|
|
|
| |
expressions; they might not yet fully work for polymorphic maps.
|
| |
|
|
|
|
| |
are run.
|
|
|