From 507b50ed1ccc51bbd24f3cea6f3c287b97b3d299 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 29 Jun 2011 16:49:45 -0700
Subject: Dafny: Fixed axioms for Seq#Contains vs. the sequence building
 functions

---
 Test/dafny0/Answer         |  7 ++++++-
 Test/dafny0/SmallTests.dfy | 16 ++++++++++++++++
 2 files changed, 22 insertions(+), 1 deletion(-)

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 29b8e708..e20f2253 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -200,8 +200,13 @@ Execution trace:
     (0,0): anon24_Then
     (0,0): anon15
     (0,0): anon25_Else
+SmallTests.dfy(347,12): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon8_Then
+    (0,0): anon7
 
-Dafny program verifier finished with 43 verified, 14 errors
+Dafny program verifier finished with 44 verified, 15 errors
 
 -------------------- Definedness.dfy --------------------
 Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index ac7286e9..8393b1c7 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -330,3 +330,19 @@ class SomeType
     }
   }
 }
+
+// ----------------------- tests of some theory axioms --------
+
+method TestSequences0()
+{
+  var s := [0, 2, 4];
+  if (*) {
+    assert 4 in s;
+    assert 0 in s;
+    assert 1 !in s;
+  } else {
+    assert 2 in s;
+    assert exists n :: n in s && -3 <= n && n < 2;
+  }
+  assert 7 in s;  // error
+}
-- 
cgit v1.2.3