summaryrefslogtreecommitdiff
path: root/Test
Commit message (Expand)AuthorAge
...
* Improve Dafny's ability to find fueled functions by checking the function its...Gravatar Bryan Parno2015-10-19
* Renamed ExistentialGuards... to BindingGuards...Gravatar Rustan Leino2015-10-07
* Use /env:0 to avoid full pathnames in test outputGravatar Rustan Leino2015-10-06
* Implemented resolution, verification, and (poorly performing) compilation of ...Gravatar leino2015-10-05
* Parsing and pretty printing of the new "existential guards" of the two kinds ...Gravatar leino2015-10-03
* Made /rewriteFocalPredicates:1 the defaultGravatar Rustan Leino2015-10-02
* Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/l...Gravatar Rustan Leino2015-10-02
* MergeGravatar leino2015-09-29
|\
| * Fix two test cases that failed if the path to "DafnySever.exe" contained spaces.Gravatar wuestholz2015-09-30
* | Removed specContextOnly parameter from ResolveStatement.Gravatar leino2015-09-28
* | Removed more traces of the previous resolution checks that happened during pa...Gravatar leino2015-09-28
* | Additional testsGravatar leino2015-09-28
* | Whitespace changes in test fileGravatar leino2015-09-28
* | Improvements in proofsGravatar leino2015-09-28
* | Changed computation of ghosts until pass 2 of resolution.Gravatar leino2015-09-28
* | A test file with an example of least vs greatest fixpoints.Gravatar leino2015-09-22
* | Added back in various ghost testsGravatar leino2015-09-20
* | Changes that only affect line numbers in test caseGravatar leino2015-09-20
* | Removed tabs from test fileGravatar leino2015-09-20
* | Adjusted (corrected, I think) test outputGravatar leino2015-09-20
* | Preliminary refactoring of ghost-statement computations to after type checkingGravatar leino2015-09-20
|/
* Proof that Ackermann can be curried and that it is monotonic in both arguments.Gravatar Rustan Leino2015-09-08
* MergeGravatar Clément Pit--Claudel2015-09-02
|\
* | Fix some tests by locally disabling auto triggersGravatar Clément Pit--Claudel2015-08-28
* | Add a small test from a discussion with BryanGravatar Clément Pit--Claudel2015-08-28
* | Implement workarounds for some tests that fail with /autoTriggers.Gravatar Clément Pit--Claudel2015-08-28
* | Suppress many warnings in the test suite.Gravatar Clément Pit--Claudel2015-08-28
* | Clarify a commentGravatar Clément Pit--Claudel2015-08-28
* | Implement {:nowarn}, clarify some messages, and add a few testsGravatar Clément Pit--Claudel2015-08-28
| * MergeGravatar Rustan Leino2015-08-28
| |\ | |/ |/|
| * Added tests for Boogie's new /verifySnapshots:3, which will be used by the Da...Gravatar Rustan Leino2015-08-28
| * Fixed spelling mistake in test fileGravatar Rustan Leino2015-08-28
* | Add a small test from the IronClad notebookGravatar Clément Pit--Claudel2015-08-27
* | Further relax the loop detection conditionsGravatar Clément Pit--Claudel2015-08-27
* | Small fix: there is no loop in (forall x :: Q(x) && Q(0))Gravatar Clément Pit--Claudel2015-08-27
* | Improve the redundancy detection algorithm used while constructing sets of termsGravatar Clément Pit--Claudel2015-08-26
|/
* Add change missing from bd47e3cdb79cGravatar Clément Pit--Claudel2015-08-23
* s/loops with/may loop with/Gravatar Clément Pit--Claudel2015-08-23
* Added /autoTriggers to two tests where it only makes a cosmetic differenceGravatar Clément Pit--Claudel2015-08-23
* Replace b || !b by true in Snapshots5.v1.dfyGravatar Clément Pit--Claudel2015-08-23
* Make quantifier splitting a two step processGravatar Clément Pit--Claudel2015-08-23
* Improve error reporting for split quantifiersGravatar Clément Pit--Claudel2015-08-23
* Allow MultiSelectExpr as quantifier headsGravatar Clément Pit--Claudel2015-08-23
* Fix: multi-dimensional OOB errors were sometimes reported on incorrect locati...Gravatar Clément Pit--Claudel2015-08-23
* Add one more wish: it would be nice to be able to prove exists b: bool :: bGravatar Clément Pit--Claudel2015-08-22
* Grant "wishlist/useless-casts-in-decreases-clauses.dfy"Gravatar Clément Pit--Claudel2015-08-22
* Add more wishes to the wishlistGravatar Clément Pit--Claudel2015-08-22
* Look at the full quantifier to find loops, not just the term.Gravatar Clément Pit--Claudel2015-08-22
* Add a 'tutorial' folder to the distribution, with an initial example.Gravatar Clément Pit--Claudel2015-08-22
* MergeGravatar Clément Pit--Claudel2015-08-21
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 06:57:58 +0000