summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Fixed typo in INSTALL fileGravatar leino2015-09-23
* Fix #90Gravatar Clément Pit--Claudel2015-09-09
* 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 for comparison error in prelude when using /optimize.Gravatar Michael Lowell Roberts2015-08-31
* | Fix some tests by locally disabling auto triggersGravatar Clément Pit--Claudel2015-08-28
* | Align the server's default kill time with the one of the VS extensionGravatar 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
* | Put contents od release packages into a dafny/ directoryGravatar 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
* | Tiny cleanup in TriggersCollectorGravatar Clément Pit--Claudel2015-08-27
* | Add a tip to the packaging scriptGravatar Clément Pit--Claudel2015-08-27
* | Update INSTALL to reflect the latest packaging changesGravatar Clément Pit--Claudel2015-08-27
* | package.py: Keep z3's exec bits, and set the exec bit on the dafny/ scriptGravatar Clément Pit--Claudel2015-08-27
* | More fixes to the packaging scriptGravatar Clément Pit--Claudel2015-08-27
* | Make the packaging script Windows-compatibleGravatar Clément Pit--Claudel2015-08-27
* | Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience)Gravatar 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
* | MergeGravatar Clément Pit--Claudel2015-08-26
|\|
* | Improve the redundancy detection algorithm used while constructing sets of termsGravatar Clément Pit--Claudel2015-08-26
| * MergeGravatar Clément Pit--Claudel2015-08-24
|/|
| * Add the Package folder to .hgignoreGravatar Clément Pit--Claudel2015-08-24
* | Add change missing from bd47e3cdb79cGravatar Clément Pit--Claudel2015-08-23
* | s/loops with/may loop with/Gravatar Clément Pit--Claudel2015-08-23
* | MergeGravatar Clément Pit--Claudel2015-08-23
|\|
| * Write a new packaging script for DafnyGravatar Clément Pit--Claudel2015-08-23
| * Replace the Emacs mode files by a pointer to the boogie-friends repo.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
* | Shallow-copy quantifier attributes when splittingGravatar Clément Pit--Claudel2015-08-23
* | Add a sanity check in QuantifiersCollectionGravatar 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
* | Trivial code cleanupGravatar Clément Pit--Claudel2015-08-23
* | Exclude axiom-profiler.html and z3.log files in the Test directoryGravatar Clément Pit--Claudel2015-08-23
* | Fix: multi-dimensional OOB errors were sometimes reported on incorrect locati...Gravatar Clément Pit--Claudel2015-08-23
* | Ignore .bpl files in the Test directoryGravatar Clément Pit--Claudel2015-08-22
* | 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
* | Ignore flycheck_ and .orig filesGravatar Clément Pit--Claudel2015-08-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-18 13:18:51 +0000