1 files changed, 33 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 043a4cfd..d1584333 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -30,6 +30,21 @@ class MyClass<T, U> {
       assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
     }
   }
+
+  function F(x: int, y: int, h: WildData, k: WildData): WildData
+  {
+    if x < 0 then
+      h
+    else if x == 0 then
+      if if h == k then true else false then
+        h
+      else if y == 0 then
+        k
+      else
+        h
+    else
+      k
+  }
 }
 
 datatype List<T> {
@@ -70,8 +85,25 @@ TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C
 SmallTests.dfy(30,7): Error: RHS expression must be well defined
 Execution trace:
     (0,0): anon0
+SmallTests.dfy(61,36): Error: possible division by zero
+Execution trace:
+    (0,0): anon0
+    (0,0): anon10_Then
+SmallTests.dfy(62,51): Error: possible division by zero
+Execution trace:
+    (0,0): anon0
+    (0,0): anon10_Else
+    (0,0): anon3
+    (0,0): anon11_Else
+SmallTests.dfy(63,22): Error: target object may be null
+Execution trace:
+    (0,0): anon0
+    (0,0): anon10_Then
+    (0,0): anon3
+    (0,0): anon11_Then
+    (0,0): anon6
 
-Dafny program verifier finished with 4 verified, 1 error
+Dafny program verifier finished with 6 verified, 4 errors
 
 -------------------- Queue.dfy --------------------