summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
| * | MergeGravatar Rustan Leino2011-06-29
| |\ \
| * | | Boogie: use (WEIGHT 0) with the select-of-store axiomsGravatar Rustan Leino2011-06-29
| * | | Dafny: Fixed axioms for Seq#Contains vs. the sequence building functionsGravatar Rustan Leino2011-06-29
* | | | Initial implementation of return statments with parameters.Gravatar Jason Koenig2011-06-29
| |/ / |/| |
* | | Removed development comments.Gravatar Jason Koenig2011-06-29
* | | MergeGravatar Jason Koenig2011-06-29
|\ \ \
* | | | Added regression test file LoopModifies.dfy.Gravatar Jason Koenig2011-06-29
| * | | Boogie build succeeded, 1 test(s) failedGravatar CodeplexBot2011-06-29
|/ / /
* | | MergeGravatar Jason Koenig2011-06-28
|\ \ \
* | | | Added regression test for loop modifies clauses.Gravatar Jason Koenig2011-06-28
* | | | Changed regression test answer for dafny0 to reflect new error messages.Gravatar Jason Koenig2011-06-28
* | | | Initial modifies on loops implementation. Still some errors remaining.Gravatar Jason Koenig2011-06-28
| * | | ported all the counterexample code to Michal's new Model class; the goal is t...Gravatar Unknown2011-06-27
|/ / /
* | | Boogie build succeededGravatar CodeplexBot2011-06-27
* | | Fixed non-incremental option of stratified inliningGravatar Unknown2011-06-27
* | | FindLeastToVerify: accept multiple proceduresGravatar Unknown2011-06-26
* | | Call PostOrderVisitIterative by defaultGravatar Unknown2011-06-26
* | | Added an iterative version of PostOrderVisit (but it is not called)Gravatar Unknown2011-06-26
* | | Avoid restarting the theorem prover for stratified inlining because itGravatar Unknown2011-06-25
* | | early clearing of live variables and incarnation mapsGravatar qadeer2011-06-24
| | * fixed some minor bugs:Gravatar Unknown2011-06-24
| | * - implemented code generation from a synthesis solution (simple fieldGravatar Unknown2011-06-24
* | | further refactoringGravatar qadeer2011-06-24
| | * - implemented reading models from a BVD model fileGravatar Unknown2011-06-24
* | | MergeGravatar qadeer2011-06-24
|\ \ \
* | | | extra test filesGravatar qadeer2011-06-24
* | | | fixes to z3apiGravatar qadeer2011-06-24
| * | | Boogie build succeededGravatar CodeplexBot2011-06-24
|/ / /
* | | MergeGravatar qadeer2011-06-23
|\ \ \
* | | | implementation of iterative LetVCGravatar qadeer2011-06-23
| * | | MergeGravatar Jason Koenig2011-06-23
| |\ \ \
| * | | | Added loop modifies clause syntax.Gravatar Jason Koenig2011-06-23
| | |/ / | |/| |
* | | | MergeGravatar qadeer2011-06-23
|\ \ \ \ | | |/ / | |/| |
* | | | bug fix in translation of dispatch continuationGravatar qadeer2011-06-23
| * | | Didn't intend to include Z3api by defaultGravatar Unknown2011-06-23
| * | | Bug fix for trace generation with extractLoop optionGravatar Unknown2011-06-23
| |\ \ \ | |/ / / |/| | |
| * | | Bug fix for trace generation with extractLoop optionGravatar Unknown2011-06-23
* | | | clean up in z3apiGravatar qadeer2011-06-22
|/ / /
* | | MergeGravatar qadeer2011-06-22
|\| |
* | | partial fixes to these regressionsGravatar qadeer2011-06-22
* | | various fixes to port to latest version of Microsoft.Z3.dllGravatar qadeer2011-06-22
| * | MergeGravatar Rustan Leino2011-06-21
| |\ \ | |/ / |/| |
| * | Dafny: bug fix in generating IsCanonicalBoolBox predicatesGravatar Rustan Leino2011-06-21
* | | MergeGravatar qadeer2011-06-20
|\| |
* | | Translate IConditional exactly the same way as IConditionalStatement to accou...Gravatar qadeer2011-06-20
| * | MergeGravatar Rustan Leino2011-06-20
| |\ \ | |/ / |/| |
| * | Dafny: better error message when "decreases *" is attempted on a function or ...Gravatar Rustan Leino2011-06-20
* | | MergeGravatar qadeer2011-06-20
|\| |
* | | whole bunch of bug fixesGravatar qadeer2011-06-20
| * | MergeGravatar Rustan Leino2011-06-20
| |\ \