From 5bb7ad4c69ed1c782e50272d37bf116007a52f4c Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Thu, 19 Nov 2015 14:39:36 -0600
Subject: Fix issue with partially-verified assertions.

---
 Test/test1/AssertVerifiedUnder0.bpl | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 Test/test1/AssertVerifiedUnder0.bpl

(limited to 'Test/test1/AssertVerifiedUnder0.bpl')

diff --git a/Test/test1/AssertVerifiedUnder0.bpl b/Test/test1/AssertVerifiedUnder0.bpl
new file mode 100644
index 00000000..e419a5ef
--- /dev/null
+++ b/Test/test1/AssertVerifiedUnder0.bpl
@@ -0,0 +1,8 @@
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0()
+{
+    assert {:verified_under 4} true;
+    assert {:verified_under 3.0} true;
+}
-- 
cgit v1.2.3