Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ↵ | Rustan Leino | 2011-10-27 |
| | | | | The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated. | ||
* | added a new regression | qadeer | 2011-07-09 |
| | |||
* | fixed bug in vcgen for bitvectors | qadeer | 2011-07-09 |
| | |||
* | Updated parser.cs files to pick up the new .frame improvements from ↵ | rustanleino | 2010-10-26 |
| | | | | boogiepartners | ||
* | Boogie: Fixed test 'bitvectors'. | wuestholz | 2010-08-14 |
| | |||
* | Fix the test to use new name for /z3bv option. | MichalMoskal | 2010-08-10 |
| | |||
* | Boogie: added /z3bv option that overrides the current setting of Z3 options ↵ | stobies | 2010-08-06 |
| | | | | for better performance on VCs that are heavy on bitvector arithmetic | ||
* | Remove vcc1 testcase that never worked with Boogie2 and is testing obsolete ↵ | MichalMoskal | 2009-12-17 |
| | | | | bvInt handling in Boogie | ||
* | Fixed some bugs in the generation of bitvector input for Z3. | rustanleino | 2009-09-29 |
| | | | | Deleted/ignored some binaries in the Binaries directory. | ||
* | Removed Output files. These are created on a local machine when the tests ↵ | rustanleino | 2009-08-07 |
| | | | | are run. | ||
* | Initial set of files. | mikebarnett | 2009-07-15 |