Dafny:

* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks

1 files changed, 10 insertions, 0 deletions

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index ba6c8e0c..4e3fab69 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -150,4 +150,14 @@ class Modifies {
       m.x := m.x + 1;  // error: may violate modifies clause

     }

   }

+

+  method SetConstruction() {

+    var s := {1};

+    assert s != {};

+    if (*) {

+      assert s != {0,1};

+    } else {

+      assert s != {1,0};

+    }

+  }

 }