Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Boogie: Yet another refinement of how Z3 is found. Previously, it would ↵ | 2011-02-09 | |
| | | | | only look in one of "c:\Program Files\Microsoft Research" and "c:\Program Files (x86)\Microsoft Research", even if both existed (which meant that it might have looked in the wrong one). Now, both are considered. | ||
* | Look for z3.exe in the prover plugin directory first. | 2011-02-02 | |
| | |||
* | Boogie: Made the algorithm for finding Z3 more robust. | 2011-01-21 | |
| | |||
* | Use a made-up name when Context.Lookup() cannot find a name | 2010-12-10 | |
| | |||
* | Don't crash in Context.Lookup when the namer has never seen the name. This ↵ | 2010-12-10 | |
| | | | | happens when the name is never used in the VC (e.g. it gets peep-hole optimized). | ||
* | Boogie: Look for Z3 versions up to 2.20. | 2010-11-23 | |
| | |||
* | Boogie: Changed the trace output formatting of the prover version slightly. | 2010-11-11 | |
| | |||
* | Boogie: | 2010-10-12 | |
| | | | | | | * enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting | ||
* | Boogie: Commented out all occurences of repeated inherited contracts - makes ↵ | 2010-08-27 | |
| | | | | fewer error messages when compiling with runtime checking on. | ||
* | Boogie: Fixed some doubly-inherited-contract occurrences. | 2010-08-20 | |
| | |||
* | Boogie: Fixed some doubly-inherited-contract occurrences. | 2010-08-20 | |
| | |||
* | Boogie: added /z3bv option that overrides the current setting of Z3 options ↵ | 2010-08-06 | |
| | | | | for better performance on VCs that are heavy on bitvector arithmetic | ||
* | Boogie: Committing my port of simplify, along with the slightly changed ↵ | 2010-07-23 | |
| | | | | references of simplify's dependents. | ||
* | Boogie: Renaming Simplify.sscproj and source files in preparation for ↵ | 2010-07-23 | |
committing my port of Simplify.csproj. |