| 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.
|
|
|
|
|
|
|
|
|
|
| |
The following tests will probably fail for newer versions
of Z3 (e.g. 4.3)
stratifiedinline/bar10.bpl
stratifiedinline/bar7.bpl
stratifiedinline/bar8.bpl
stratifiedinline/bar9.bpl
|
| |
|
|
|
|
|
| |
Reduce depth of AST whenever possible (e.g., use a binary tree instead of a
linear list of terms)
|
| |
|
| |
|
|
|
|
| |
added /vc:i to all tests in stratifiedinline
|
| |
|
| |
|
|
|
|
| |
stratified inliinig is now run always with /doNotUseLabels
|
|
|
|
| |
Don't use UNSAT core for the refinement step.
|
|
|
|
| |
added regressions
|
|
|
|
| |
The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
|
| |
|
|
|
|
|
|
|
|
| |
* Added internal support for multi-dimensional arrays (but not all surface syntax is there yet)
* Removed unused variables from Dafny.atg
Boogie and Dafny:
* Improved error message for postcondition violations
|
|
/stratifiedInline:1.
|