summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* 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
| * 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
| |\
| * | Dafny: Commented out SnapshotableTrees.Node.FunctionalInsert while performanc...Gravatar Rustan Leino2011-10-26
| * | BVD: fixed two basic but damning problems with the Dafny provider, and elided...Gravatar Rustan Leino2011-10-26
| | * Added batch script to run tests for datatypes tests.Gravatar Mike Barnett2011-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
|/
* MergeGravatar Rustan Leino2011-10-24
|\
* | Dafny: continued translation of "parallel" statements (Assign and Proof forms...Gravatar Rustan Leino2011-10-24
| * Don't let /s be specified for stub files. (But keep the old code in case weGravatar Mike Barnett2011-10-23
* | 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
| * Tagging EMIC CC.NET build 2.1.31022.0Gravatar VccBuildServer2011-10-22
| * 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
| * Boogie build succeededGravatar CodeplexBot2011-10-20
| * 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
| * | Tagging EMIC CC.NET build 2.1.31020.0Gravatar VccBuildServer2011-10-20
| |/
| * MergeGravatar Michal Moskal2011-10-19
| |\ | |/ |/|
| * Performance improvements in BVDGravatar Michal Moskal2011-10-19
* | MergeGravatar Rustan Leino2011-10-19
|\|
* | Jennisys: added "ensures" to emacs modeGravatar Rustan Leino2011-10-19
| * Tagging EMIC CC.NET build 2.1.31019.0Gravatar VccBuildServer2011-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
| * Boogie build succeededGravatar CodeplexBot2011-10-18
| * added houdini to regressionGravatar qadeer2011-10-17
| * Boogie build succeededGravatar CodeplexBot2011-10-17
| * MergeGravatar qadeer2011-10-16
| |\
| * | revised implementation of proc copy boundingGravatar qadeer2011-10-16
| | * Boogie build succeededGravatar CodeplexBot2011-10-14
| |/ |/|
* | Jennisys: changed the fixpoint solver to pick only the true clause in a disju...Gravatar Unknown2011-10-10
* | Jennisys: implemented minimization of inferred guardsGravatar Unknown2011-10-10