summaryrefslogtreecommitdiff
path: root/Test/test2
Commit message (Expand)AuthorAge
* MergeGravatar Pantazis Deligiannis2013-07-15
|\
* | Added an attribute to set the time limit for implementations.Gravatar wuestholz2013-07-12
| * added python scripts (work in unix and windows) for testing Z3 and CVC4 to ma...Gravatar Pantazis Deligiannis2013-07-07
|/
* Changed the prover interface to report traces for time outs and out of memory.Gravatar wuestholz2013-05-30
* Fixed bug in the cutting of back edges (that manifested itself whenever the f...Gravatar Rustan Leino2013-05-29
* removed call forall and * args to callsGravatar Unknown2013-02-23
* Boogie: added type 'real' with overloaded arithmetic operations plus real div...Gravatar boehmes2012-09-27
* Boogie: new syntax for integer division and modulus: use div and mod instead ...Gravatar boehmes2012-09-27
* Updated the 'Answer' file for test2.Gravatar wuestholz2011-12-02
* Boogie: Fixed a crash due to old expressions in lambda expressions that were ...Gravatar wuestholz2011-12-02
* Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ...Gravatar Rustan Leino2011-10-27
* Added "free call" statements that don't check the precondition in the caller.Gravatar wuestholz2011-09-14
* Fix a bug in cloning of nested lambda expressions in AI engineGravatar MichalMoskal2011-02-11
* Add description of {:selective_checking} to the /attrHelp. Fix the testcase.Gravatar MichalMoskal2011-01-13
* Add new feature: {:selective_checking} on procedures. See testcase for a desc...Gravatar MichalMoskal2010-12-17
* Boogie:Gravatar rustanleino2010-10-26
* Dafny:Gravatar rustanleino2010-09-14
* Change Synonym type printing to what it was, use a workaround in TypeToString...Gravatar MichalMoskal2010-08-18
* Boogie:Gravatar rustanleino2010-05-15
* Dafny: Added definedness checks for all statements (previously, some were mi...Gravatar rustanleino2010-03-13
* Boogie:Gravatar rustanleino2010-02-20
* Fix up the polymorphic case for lambda; it probably still isn't quite correct.Gravatar MichalMoskal2010-02-19
* Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda expressions;...Gravatar MichalMoskal2010-02-19
* Implement if-then-else expression.Gravatar MichalMoskal2010-02-18
* Implemented block coalescing invoked right after type checking.Gravatar qadeer2010-02-16
* Updated Answer files, in synch with my recent edits 31961.Gravatar rustanleino2009-08-16
* Removed Output files. These are created on a local machine when the tests ar...Gravatar rustanleino2009-08-07
* Initial set of files.Gravatar mikebarnett2009-07-15