summaryrefslogtreecommitdiff
path: root/Test/snapshots/Snapshots0.v2.bpl
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2013-06-02 18:16:30 -0700
committerGravatar wuestholz <unknown>2013-06-02 18:16:30 -0700
commit734ee394898d9e37c784f32e0d105678f82d981a (patch)
tree16a650a0da1d5e03f7675bfc930669e708f31342 /Test/snapshots/Snapshots0.v2.bpl
parent5aaf3b555f7ffd81468d95f1d543f5f1212f6643 (diff)
Added a feature for verifying several program snapshots (incl. result caching and prioritization).
Diffstat (limited to 'Test/snapshots/Snapshots0.v2.bpl')
-rw-r--r--Test/snapshots/Snapshots0.v2.bpl31
1 files changed, 31 insertions, 0 deletions
diff --git a/Test/snapshots/Snapshots0.v2.bpl b/Test/snapshots/Snapshots0.v2.bpl
new file mode 100644
index 00000000..156977f7
--- /dev/null
+++ b/Test/snapshots/Snapshots0.v2.bpl
@@ -0,0 +1,31 @@
+// id = "P0:1"
+// priority = 5
+// checksum = "012"
+//
+// Action: skip
+procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()
+{
+ assert false;
+}
+
+
+// id = "P1:0"
+// priority = 1
+// checksum = "234"
+//
+// Action: skip
+procedure {:priority 1} {:checksum "234"} P1()
+{
+ assert true;
+}
+
+
+// id = "P3:0"
+// priority = 1
+// checksum = "234"
+//
+// Action: skip
+procedure {:checksum "234"} P3()
+{
+ assert true;
+}