summaryrefslogtreecommitdiff
path: root/Binaries
Commit message (Expand)AuthorAge
* Auto-merged heads.Gravatar Michael Lowell Roberts2015-09-21
|\
| * Fix a check that occasionally led to an out of bounds exception in the extensionGravatar Bryan Parno2015-09-17
* | Fix for soundness bug discovered in SeqFromArray.Gravatar Michael Lowell Roberts2015-09-17
|/
* Fix #90Gravatar Clément Pit--Claudel2015-09-09
* fix for comparison error in prelude when using /optimize.Gravatar Michael Lowell Roberts2015-08-31
* Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience)Gravatar Clément Pit--Claudel2015-08-27
* Set exec flag on Binaries/z3Gravatar Clément Pit--Claudel2015-08-22
* Fixed compilation that involve enumeration over native-type newtype values.Gravatar Rustan Leino2015-08-20
* Add a wrapper script around the Dafny binary (for mono).Gravatar Clément Pit--Claudel2015-08-13
* Add a Linux z3 binary to the repo, and use that or z3.exe based on the OSGravatar Clément Pit--Claudel2015-07-31
* Update z3 to 4.4. One test had to be edited.Gravatar Clément Pit--Claudel2015-07-21
* Fixed bug in BplImp!Gravatar leino2015-07-01
* Tried to reduce frame-axiom instantiations by saying the earlier heap must be...Gravatar leino2015-06-25
* System.Collections.Immutable.dll is now stored in the Binaries directory and ...Gravatar Michael Lowell Roberts2015-06-16
* added -optimize option to compiler.Gravatar Michael Lowell Roberts2015-06-12
* Fix the Seq#Contain axiom; it should talk about T, not ref.Gravatar Clément Pit--Claudel2015-06-07
* Add an infinite set collection type.Gravatar qunyanm2015-05-29
* Bumped version to 1.9.4.20428Gravatar leino2015-04-29
* HashCode for Set/MultiSet/Map should be independent of the order of theGravatar qunyanm2015-04-17
* Change GetHashCode for Set, MultiSet and MapGravatar qunyanm2015-04-16
* Fix issue #68. Change GetHashCode implementation for Sequence.Gravatar qunyanm2015-04-14
* MergeGravatar qunyanm2015-04-06
|\
* | Add z3.exe and z3-license.txt to dafny binary and extension distribution.Gravatar qunyanm2015-04-06
| * Fixed some bugs in override axioms (but still missing support for classes wit...Gravatar leino2015-04-05
|/
* Add LongLength methods to Set/Map in DafnyRuntime.csGravatar chrishaw2015-03-17
* Beefed up collection axioms (in particular, for maps) to improve the chance o...Gravatar Rustan Leino2015-03-10
* Removed some old and unused functionsGravatar leino2015-03-09
* Fix issue #60Gravatar qunyanm2015-03-06
* Add imap display/update expressionsGravatar chrishaw2015-02-27
* Add imap type, which is like map but may have have infinite sizeGravatar chrishaw2015-02-26
* Optimization to nativeType: have EuclideanModulus_sbyte and EuclideanModulus_...Gravatar chrishaw2014-12-11
* Optimization to nativeType: have EuclideanDivision_sbyte and EuclideanDivisio...Gravatar chrishaw2014-12-09
* Add nativeType attribute for newtype declarations. Change Compiler.cs to use...Gravatar chrishaw2014-12-09
* Various DafnyPrelude.bpl cleanup.Gravatar leino2014-11-01
* Improved power of axioms Seq#FromArrayGravatar leino2014-10-31
* 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
|/