summaryrefslogtreecommitdiff
path: root/Test/prover
Commit message (Collapse)AuthorAge
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-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.
* Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has aGravatar Dan Liew2015-04-26
| | | | | variable that begins with a ``.``. This was't an issue for Z3 which ignores this but CVC4 is stricter and will emit an error
* Removed old test infrastructure files except forGravatar Dan Liew2014-05-28
| | | | | | | | | ./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete.
* Fix lit test suite when running Boogie under a path that containsGravatar Dan Liew2014-05-27
| | | | spaces.
* Enabled prover lit tests.Gravatar Dan Liew2014-05-07
|
* Changed the 'CounterexampleComparer' to take traces into account.Gravatar wuestholz2013-05-26
|
* added parallel callsGravatar Unknown2013-03-01
|
* Boogie and Dafny: adjustments to the test suite expected output (and a ↵Gravatar Unknown2012-09-27
| | | | temporary hack in FloydCycleDetect.dfy to be corrected shortly)
* Boogie: new syntax for integer division and modulus: use div and mod instead ↵Gravatar boehmes2012-09-27
| | | | of / and %
* Add tests for -z3multipleErrors from Shuvendu.Gravatar MichalMoskal2011-02-23