Revised the $Is and $IsAlloc axioms for arrow terms. It is now possible to

derived these predicates.  More things can now be verified (including the
problem reported in Issue #49).

2 files changed, 5 insertions, 6 deletions

diff --git a/Test/hofs/OneShot.dfy b/Test/hofs/OneShot.dfy
index 286be898..e920530a 100644
--- a/Test/hofs/OneShot.dfy
+++ b/Test/hofs/OneShot.dfy
@@ -10,16 +10,15 @@ method OneShot() {
   var i : Ref<int>;
   i := new Ref;
 
-  g := () -> true;
-
+  g := () reads i -> true;  // using a (deprecated) one-shot arrow here means "g" acquires
+                           // a precondition that says it can only be applied in this heap
   assert g();
 
   i.val := i.val + 1; // heap changes
 
   if * {
-    assert g();         // should fail
+    assert g();         // error: precondition violation
   } else {
-    assert !g();        // should fail
+    assert !g();        // error: precondition violation
   }
 }
-
diff --git a/Test/hofs/VectorUpdate.dfy b/Test/hofs/VectorUpdate.dfy
index ca6b20b3..6fb25a87 100644
--- a/Test/hofs/VectorUpdate.dfy
+++ b/Test/hofs/VectorUpdate.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %dafny /compile:3 /autoTriggers:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // this is a rather verbose version of the VectorUpdate method