summaryrefslogtreecommitdiff
path: root/Test/bitvectors
Commit message (Collapse)AuthorAge
* Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ↵Gravatar Rustan Leino2011-10-27
| | | | The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
* added a new regressionGravatar qadeer2011-07-09
|
* fixed bug in vcgen for bitvectorsGravatar qadeer2011-07-09
|
* Updated parser.cs files to pick up the new .frame improvements from ↵Gravatar rustanleino2010-10-26
| | | | boogiepartners
* Boogie: Fixed test 'bitvectors'.Gravatar wuestholz2010-08-14
|
* Fix the test to use new name for /z3bv option.Gravatar MichalMoskal2010-08-10
|
* Boogie: added /z3bv option that overrides the current setting of Z3 options ↵Gravatar stobies2010-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 ↵Gravatar MichalMoskal2009-12-17
| | | | bvInt handling in Boogie
* Fixed some bugs in the generation of bitvector input for Z3.Gravatar rustanleino2009-09-29
| | | | Deleted/ignored some binaries in the Binaries directory.
* Removed Output files. These are created on a local machine when the tests ↵Gravatar rustanleino2009-08-07
| | | | are run.
* Initial set of files.Gravatar mikebarnett2009-07-15