Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merging complete. Everything looks good *crosses fingers* | Checkmate50 | 2016-06-06 |
| | |||
* | Made 2 invariants of class 'CommandLineOptions' robust by: | wuestholz | 2015-01-09 |
| | | | | | | | - making fields private - exposing IEnumerables - adding methods 'AddProverOption', 'RemoveAllProverOptions', and 'AddZ3Option' (with help from David Rohr) | ||
* | Patch by Nathan Chong: iterative version of remove empty blocks algorithm. ↵ | Ally Donaldson | 2013-12-02 |
| | | | | This appears to fix a small deficiency in the original recursive implementation, so now a larger number of empty blocks are removed. As a result, various tests produce slightly different counterexamples and have been updated to reflect this. Also, default VC generation strategy has been changed to DAGIterative, to avoid stack overflow problems. | ||
* | Removed old comments about "BASEMOVE" and other constructor calls, where the ↵ | Unknown | 2013-01-07 |
| | | | | conversion from Spec# into C# moved a constructor call | ||
* | Implement support for alternative SMT solvers -- CVC3 and CVC4 | Peter Collingbourne | 2012-09-06 |
| | |||
* | Boogie: internal clean-up, removed BvHandling type, everything now behaves ↵ | Rustan Leino | 2011-10-27 |
| | | | | as if the old /bv:z were used | ||
* | Add PROVER_PATH prover option (to base options, but currently only used by ↵ | Michal Moskal | 2011-08-29 |
| | | | | | | SMTLib) Add support for Inspector with latest Z3/SMT2 frontend | ||
* | Allow : instead of = in options | Michal Moskal | 2011-06-30 |
| | |||
* | Get rid of -smtOutput option. Add /proverOpt:OUTPUT=... to SMT and TPTP ↵ | MichalMoskal | 2011-02-11 |
| | | | | provers. Add handling of help message about /proverOpt. | ||
* | Boogie: Committing changed source files | tabarbe | 2010-08-20 |
| | |||
* | Boogie: Renaming core sources in preparation for port commit | tabarbe | 2010-08-20 |