diff options
| author |  wuestholz <unknown> | 2014-10-29 14:11:54 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-10-29 14:11:54 +0100 |
| commit | c8c15f672dc42fca1db9b0f20549ef49b48889e8 (patch) | |
| tree | 9a23b4712b94ad321d5310298f964f939c409570 /Test/snapshots/Snapshots29.v0.bpl | |
| parent | b287f7ffe5df2dadbc581acc2fb86b9e90a5a77d (diff) | |
Added a test for the verification result caching.
Diffstat (limited to 'Test/snapshots/Snapshots29.v0.bpl')
| -rw-r--r-- | Test/snapshots/Snapshots29.v0.bpl | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/Test/snapshots/Snapshots29.v0.bpl b/Test/snapshots/Snapshots29.v0.bpl new file mode 100644 index 00000000..f4087f90 --- /dev/null +++ b/Test/snapshots/Snapshots29.v0.bpl @@ -0,0 +1,15 @@ +procedure {:checksum "0"} P();
+
+implementation {:id "P"} {:checksum "1"} P()
+{
+ var i: int;
+
+ i := 0;
+
+ while (*)
+ {
+ i := 0;
+ }
+
+ assert i == 0;
+}
|