summaryrefslogtreecommitdiff
path: root/Test/dafny0/SplitExpr.dfy
Commit message (Collapse)AuthorAge
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
|
* Fixed bug where free conditions preceded checked conditions (for inlined ↵Gravatar Rustan Leino2013-12-16
| | | | predicates)
* Split verification of quantifier expressions into #2 for checked and #1 for ↵Gravatar Rustan Leino2013-01-23
| | | | | | assumed. Fixed cases where token was not being updated for refinement.
* Dafny:Gravatar rustanleino2010-06-19
* Improved design and implementation of SplitExpr * Fixed some tests in dafny0/Use.dfy * Added test case (in dafny0/Termination.dfy) to test the recent strengthening of set axioms