summaryrefslogtreecommitdiff
path: root/Binaries
Commit message (Expand)AuthorAge
* Add an option to use reduce Z3's knowledge of non-linear arithmetic.Gravatar Bryan Parno2014-10-24
* Changed version to 1.9.1.11021Gravatar leino2014-10-21
* Comparisons and well-founded order of charGravatar leino2014-10-21
* Added types "char" and "string" (the latter being a synonym for "seq<char>").Gravatar leino2014-10-20
* Fixed bugs in previous check-inGravatar leino2014-08-25
* Added .Trunc field to real-based typesGravatar leino2014-08-21
* Compile lambda functions and apply expressions, and change let expr compilationGravatar Dan Rosén2014-08-12
* MergeGravatar Dan Rosén2014-08-11
|\
* | Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-08-11
| * Implemented missing routine in runtime system (real-to-int conversion)Gravatar leino2014-07-21
|/
* MergeGravatar Dan Rosén2014-07-07
|\
* | New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
| * Added some axioms about seq-to-multiset conversionsGravatar Rustan Leino2014-06-24
| * Specialized Lit function for int and real (leaving all other cases polymorphi...Gravatar Rustan Leino2014-06-10
| * Improved axiom that knows that array-to-sequence converstion depends only on ...Gravatar Rustan Leino2014-06-04
|/
* Compile realsGravatar Rustan Leino2014-04-13
* Improvements in sequence axioms to make checking more automatic.Gravatar Rustan Leino2014-04-02
* Added axiom to transfer array element-type information onto the elements them...Gravatar Rustan Leino2014-03-20
* Fixed problem with propagating allocation information about array elements.Gravatar Rustan Leino2014-03-20
* Removed an apparently unneeded trigger.Gravatar Rustan Leino2014-03-06
* Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for lite...Gravatar Rustan Leino2014-02-13
* Preliminary support for reals in Dafny specs. No compiler suport yet.Gravatar Bryan Parno2014-02-10
* MergeGravatar Rustan Leino2014-01-08
|\
* | Allow left-hand sides of a let expression to be patterns (like in the case of...Gravatar Rustan Leino2014-01-08
| * Compile assign-such-that for all integers, not just ones where a bound is foundGravatar Rustan Leino2014-01-06
|/
* Print and translate "match" expressions in general positions, not just at the...Gravatar Rustan Leino2014-01-03
* Embellished axioms about GenericAlloc and DtAlloc.Gravatar Rustan Leino2014-01-03
* Fix some things due to changes in Boogie (execution engine API, 'UnivBackPred...Gravatar wuestholz2013-12-09
* Fixed build failures due to changes in Boogie.Gravatar wuestholz2013-11-23
* Fixed typo in build scriptGravatar Rustan Leino2013-08-06
* MergeGravatar Rustan Leino2013-08-06
|\
| * Updated 'PrepareDafnyZip.bat'.Gravatar wuestholz2013-08-05
* | Unified function/method context heightsGravatar Rustan Leino2013-08-04
|/
* Changed the encoding of recursive functions. Previous, three hardcoded layer...Gravatar Rustan Leino2013-08-02
* Axioms that relate (multi)set cardinality with (multi)set difference.Gravatar Rustan Leino2013-07-16
* Computations!Gravatar Unknown2013-07-04
* Changed ranking function for Seq, so that it's compatible with data types.Gravatar Unknown2013-06-26
* Beefed up axioms about cardinality and the empty (multi)set, which fixes Issu...Gravatar Rustan Leino2013-06-20
* Removed the set cardinality/subset axiom (with no trigger, it caused test sui...Gravatar Rustan Leino2013-04-02
* Updated cardinality axioms for sets.Gravatar Nadia Polikarpova2013-03-30
* The "choose" statement, hacky and specialized as it was, is now gone. Use th...Gravatar Rustan Leino2013-03-27
* Replaced SuperSetBoundedPool by SubSetBoundedPool, which is much more useful ...Gravatar Rustan Leino2013-03-27
* First take on set, multiset and map cardinality.Gravatar Nadia Polikarpova2013-03-22
* Bumped version to 1.6.1, to be released as a binary and on rise4fun.Gravatar Rustan Leino2013-03-10
* Disallow allocations in ghost contextsGravatar Rustan Leino2013-03-06
* Encode codatatype equalities by predefined copredicates, including their pref...Gravatar Rustan Leino2013-01-15
* Include BVD in build (to copy it into the Dafny\Binaries directory)Gravatar Unknown2012-10-30
* Test cases for co-inductive proofs, and an axiom that makes some of them poss...Gravatar Rustan Leino2012-10-19
* Added some axioms to try to recover boxed data. In particular, any element '...Gravatar Unknown2012-10-17
* Change the encoding of proof certificates to make the two levels explicitGravatar Unknown2012-10-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 21:54:23 +0000