summaryrefslogtreecommitdiff
path: root/Test/dafny0/snapshots/Snapshots1.v1.dfy
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-07-03 03:22:45 +0200
committerGravatar wuestholz <unknown>2014-07-03 03:22:45 +0200
commitbebfbaa98ac099cba47cfd1f02e6781ea257997f (patch)
treeecc198613e10399f0a7aaf8ff033229e0ffc55c8 /Test/dafny0/snapshots/Snapshots1.v1.dfy
parent61f46d7b7789290098361c2de7e775fbe487bd7f (diff)
Changed "dummy" checksums to "stable" and added more tests for the verification result caching.
Diffstat (limited to 'Test/dafny0/snapshots/Snapshots1.v1.dfy')
-rw-r--r--Test/dafny0/snapshots/Snapshots1.v1.dfy13
1 files changed, 13 insertions, 0 deletions
diff --git a/Test/dafny0/snapshots/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Snapshots1.v1.dfy
new file mode 100644
index 00000000..93ad6068
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots1.v1.dfy
@@ -0,0 +1,13 @@
+method M()
+{
+ N();
+ assert false; // error
+}
+
+method N()
+ ensures P;
+
+predicate P
+{
+ true
+}