Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Cleaned up a test program | Rustan Leino | 2014-07-08 |
* | Invert LHS sub-expressions in forall assignment statements, which gives the o... | Rustan Leino | 2014-06-24 |
* | Set up the same test infrastructure as in Boogie. | wuestholz | 2014-05-29 |
* | Added an assert to help the theorem prover out in the RingBuffer.Enqueue method. | Rustan Leino | 2013-07-29 |
* | Changed ranking function for Seq, so that it's compatible with data types. | Unknown | 2013-06-26 |
* | Reverted some accidental changes to a test case | Rustan Leino | 2013-02-11 |
* | Renamed a variable in some test cases | Rustan Leino | 2013-02-02 |
* | Dafny: removed a now-inferred type-parameter instantiation in a test file | Unknown | 2012-03-07 |
* | Dafny: added ghost modules (the meaning is simply that such a module will not... | Rustan Leino | 2012-03-07 |
* | Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic sp... | Unknown | 2012-03-05 |