summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* MergeGravatar qadeer2011-11-07
|\
* \ MergeGravatar qadeer2011-11-07
|\ \
* | | change in model parsing with datatype valuesGravatar qadeer2011-11-07
| * | Dafny: added a new /inductionHeuristic optionGravatar Rustan Leino2011-11-04
| * | Dafny: added options to make Induction Heuristic apply to array index express...Gravatar Rustan Leino2011-11-04
* | | deleted unused codeGravatar qadeer2011-11-01
|/ /
* | MergeGravatar Rustan Leino2011-10-31
|\ \
* | | Fixed the generation of names for datatype functions to use the API forGravatar Mike Barnett2011-10-31
| * | MergeGravatar Rustan Leino2011-10-29
| |\ \ | |/ / |/| |
| * | Dafny induction:Gravatar Rustan Leino2011-10-29
* | | Boogie: Updated the error message for old versions of Z3.Gravatar wuestholz2011-10-28
* | | Boogie: Get rid of {:inline} attributes on axiomsGravatar Michal Moskal2011-10-27
* | | Boogie: Get rid of {:ignore} feature on axiomsGravatar Michal Moskal2011-10-27
* | | Boogie: Present a nice error message when Z3 of lesser version than 3.2 is foundGravatar Michal Moskal2011-10-27
* | | MergeGravatar Michal Moskal2011-10-27
|\ \ \
* | | | Restart prover after out-of-memory error; honour -restartProver optionGravatar Michal Moskal2011-10-27
| * | | Boogie: removed unreachable or unused codeGravatar Rustan Leino2011-10-27
| * | | Boogie: internal clean-up, removed BvHandling type, everything now behaves as...Gravatar Rustan Leino2011-10-27
| * | | Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ...Gravatar Rustan Leino2011-10-27
| * | | Boogie: Changed default /prover to SMTLIBGravatar Rustan Leino2011-10-27
| | | * MergeGravatar qadeer2011-10-27
| | | |\ | | |_|/ | |/| |
| | | * various refactoringsGravatar qadeer2011-10-27
| | * | Dafny: allow attributes on function/method declarations to refer to the (in- ...Gravatar Rustan Leino2011-10-26
| |/ /
| * | Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" s...Gravatar Rustan Leino2011-10-26
| * | Dafny: removed support for assigning to an array-range (that is, an assignmen...Gravatar Rustan Leino2011-10-26
| * | MergeGravatar Rustan Leino2011-10-26
| |\ \ | |/ / |/| |
| * | BVD: fixed two basic but damning problems with the Dafny provider, and elided...Gravatar Rustan Leino2011-10-26
* | | VCC: Detect wrong model filesGravatar Michal Moskal2011-10-26
| * | Dafny: implemented compilation of parallel statementsGravatar Rustan Leino2011-10-25
* | | VCC: improvements in showing arrays, addresses, and embeddingsGravatar Michal Moskal2011-10-24
| * | Dafny: check subrange restriction in parallel Assign statementGravatar Rustan Leino2011-10-24
|/ /
* | Dafny: continued translation of "parallel" statements (Assign and Proof forms...Gravatar Rustan Leino2011-10-24
* | Dafny: added translation of Assign case of the parallel statementGravatar Rustan Leino2011-10-22
* | MergeGravatar Rustan Leino2011-10-21
|\ \
* | | Dafny: changed triggers (which are never really used, anyhow) from having a s...Gravatar Rustan Leino2011-10-21
| * | Sync timeout messages with Z3 prover interfaceGravatar Michal Moskal2011-10-21
| * | Don't pass /T: option to Z3 - it kills Z3 prematurely when there are multiple...Gravatar Michal Moskal2011-10-21
| * | Improve logging when -proverOpt:VERBOSITY=1 or 2 is specifiedGravatar Michal Moskal2011-10-21
| |/
| * MergeGravatar Michal Moskal2011-10-19
| |\ | |/ |/|
| * VCC: support some more _(blob ...) buisnessGravatar Michal Moskal2011-10-19
* | MergeGravatar Rustan Leino2011-10-19
|\ \
* | | Dafny: fixed performance-buggy translation of exists, and also added some oth...Gravatar Rustan Leino2011-10-19
| | * BVD: Default to expert view; Only VCC uses that stuff now, and all VCC users ...Gravatar Michal Moskal2011-10-19
| |/
| * Performance improvements in BVDGravatar Michal Moskal2011-10-19
|/
* VCC: Fix problem with booleans being displayed as mapsGravatar Michal Moskal2011-10-19
* Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)Gravatar Unknown2011-10-19
* added houdini to regressionGravatar qadeer2011-10-17
* revised implementation of proc copy boundingGravatar qadeer2011-10-16
* added membership testsGravatar qadeer2011-10-05
* implementing datatypesGravatar qadeer2011-10-05