| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Update test output for Z3 4.4.1. |  Valentin Wüstholz | 2015-12-01 |
| | | |||
| * | Normalise line endings using a .gitattributes file. Unfortunately |  Dan Liew | 2015-06-28 |
| | | | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. | ||
| * | Fix ``Test/test15/CaptureState.bpl`` test under Linux. | Dan Liew | 2015-04-03 |
| | | |||
| * | Removed old test infrastructure files except for | Dan Liew | 2014-05-28 |
| | | | | | | | | | | ./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete. | ||
| * | Fix lit test suite when running Boogie under a path that contains | Dan Liew | 2014-05-27 |
| | | | | | spaces. | ||
| * | Remove old python testing scripts | Dan Liew | 2014-05-11 |
| | | |||
| * | Enabled "Benchmarks for error messages" lit tests. | Dan Liew | 2014-05-07 |
| | | | | | | | The test15/CaptureState.bpl test fails on Linux using (Z3 4.2) due to additional (but not meaningful) parentheses in the outputted model. | ||
| * | minor fix |  qadeer | 2014-05-05 |
| | | |||
| * | do monomorphic checking | qadeer | 2013-11-22 |
| | | |||
| * | cleaned up the OG code | qadeer | 2013-08-07 |
| | | | | | enabled it to be always on | ||
| * | fix in the answer |  Pantazis Deligiannis | 2013-07-22 |
| | | |||
| * | fix | Pantazis Deligiannis | 2013-07-22 |
| | | |||
| * | added python scripts (work in unix and windows) for testing Z3 and CVC4 to ↵ | Pantazis Deligiannis | 2013-07-07 |
| | | | | | many of the test suite dirs | ||
| * | Fixed bug in the cutting of back edges (that manifested itself whenever the ↵ | Rustan Leino | 2013-05-29 |
| | | | | | first block in a procedure was the target of a back edge) | ||
| * | Boogie and Dafny: adjustments to the test suite expected output (and a ↵ |  Unknown | 2012-09-27 |
| | | | | | temporary hack in FloydCycleDetect.dfy to be corrected shortly) | ||
| * | Updated test 'test15' that would fail with Z3 4.1 (different ordering of ↵ | wuestholz | 2012-09-12 |
| | | | | | elements in the model output). | ||
| * | Dafny and Boogie: get rid of 'static' fields in parser |  Rustan Leino | 2012-08-21 |
| | | |||
| * | Also updated test15 | Rustan Leino | 2012-08-14 |
| | | |||
| * | Boogie: updated test15/Answer (which showed as a permutation of the previous ↵ | Rustan Leino | 2012-06-29 |
| | | | | | Answer) | ||
| * | Dafny/Boogie/BVD: made Dafny plug-in for BVD work again | Rustan Leino | 2012-06-08 |
| | | |||
| * | Update to match the new model printing format |  Michal Moskal | 2012-04-30 |
| | | |||
| * | 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. | ||
| * | Updated the ANSWER file for 'test15'. | wuestholz | 2011-09-27 |
| | | |||
| * | Updates to Answer files from recent changes | rustanleino | 2011-03-01 |
| | | |||
| * | Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln | qadeer | 2010-12-01 |
| | | |||
| * | ModelViewer: | rustanleino | 2010-11-02 |
| | | | | | | | | * map back values introduced by bool_2_U and int_2_U * map back internal names for select/store to [n] and [n:=], where n is the arity of the map * added /break switch to ModelViewer * display more things (including sequences) in Dafny provider | ||
| * | Updated Answer file to go with the previous check-in. | rustanleino | 2010-11-02 |
| | | |||
| * | Skip unchagned variables in model dumps. Fix testcase | MichalMoskal | 2010-10-14 |
| | | |||
| * | Add missing Clone() when storing incarnation maps; update testcase to make ↵ | MichalMoskal | 2010-10-12 |
| | | | | | | | this clear Construct states in Model properly, nuke direct printing. | ||
| * | Boogie: | rustanleino | 2010-10-12 |
| | | | | | | | * enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting | ||
| * | Boogie: | rustanleino | 2010-09-24 |
| | | | | | | * Added Test/textbook/DivMod.bpl, which embodies a conversion between C's div/mod operators and SMT Lib's div/mod operators. * Added a rudimentary printing of variables for captured states. It doesn't attempt to print everything at this time, and it doesn't work when variables get unique-ified by @@-suffixes. A more complete implementation will be added at a later time. | ||
| * | Boogie: | rustanleino | 2010-09-23 |
| | | | | | | | * Added /mv flag as the start of a Boogie replacement for /cev * Allow attributes on assume statements * /mv looks for the assume-statement attribute :captureState with a string-literal argument | ||
| * | Boogie: Added boolean code expressions (sans well-formedness checks on the ↵ | rustanleino | 2010-08-10 |
| | | | | | input). | ||
| * | 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 |
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |