From 2e03ed114503dfa16547c06766fa683c690f9052 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Thu, 18 Feb 2010 19:58:38 +0000
Subject: Implement if-then-else expression.

---
 Test/test2/Answer | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'Test/test2/Answer')

diff --git a/Test/test2/Answer b/Test/test2/Answer
index 1e5a0d5f..230a8861 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -323,6 +323,16 @@ Execution trace:
     Implies.bpl(11,3): anon0
 
 Boogie program verifier finished with 0 verified, 2 errors
+
+-------------------- IfThenElse1.bpl --------------------
+IfThenElse1.bpl(26,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    IfThenElse1.bpl(26,3): anon0
+IfThenElse1.bpl(33,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    IfThenElse1.bpl(33,3): anon0
+
+Boogie program verifier finished with 2 verified, 2 errors
 -------------------- sk_hack.bpl --------------------
 
 Boogie program verifier finished with 1 verified, 0 errors
-- 
cgit v1.2.3