From 554fb3a6780c412b81dc935835c2760e4cbe0b4d Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Tue, 10 Aug 2010 02:16:29 +0000
Subject: Boogie: Added boolean code expressions (sans well-formedness checks
 on the input).

---
 Test/test15/Answer | 27 +++++++++++++++++++++------
 1 file changed, 21 insertions(+), 6 deletions(-)

(limited to 'Test/test15')

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 2054998f..8452acb6 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -19,6 +19,11 @@ $pow2 -> {
   *8 -> *9
   else -> #unspecified
 }
+tickleBool -> {
+  *1 -> *0
+  *0 -> *0
+  else -> #unspecified
+}
 Ctor -> {
   *4 -> *8
   *5 -> *9
@@ -50,7 +55,7 @@ False : *1
 End of model.
 NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    NullInModel.bpl(2,3): anon0
+        NullInModel.bpl(2,3): anon0
 
 Boogie program verifier finished with 0 verified, 1 error
 
@@ -71,6 +76,11 @@ $pow2 -> {
   *6 -> *7
   else -> #unspecified
 }
+tickleBool -> {
+  *1 -> *0
+  *0 -> *0
+  else -> #unspecified
+}
 Ctor -> {
   *4 -> *6
   *5 -> *7
@@ -94,7 +104,7 @@ False : *1
 End of model.
 IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    IntInModel.bpl(2,3): anon0
+        IntInModel.bpl(2,3): anon0
 
 Boogie program verifier finished with 0 verified, 1 error
 
@@ -121,6 +131,11 @@ $pow2 -> {
   *13 -> *9
   else -> #unspecified
 }
+tickleBool -> {
+  *1 -> *0
+  *0 -> *0
+  else -> #unspecified
+}
 Ctor -> {
   *4 -> *13
   *5 -> *9
@@ -159,19 +174,19 @@ False : *1
 End of model.
 ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    ModelTest.bpl(3,5): anon0
+        ModelTest.bpl(3,5): anon0
 
 Boogie program verifier finished with 0 verified, 1 error
 
 -------------------- InterpretedFunctionTests --------------------
 InterpretedFunctionTests.bpl(4,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    InterpretedFunctionTests.bpl(2,3): anon0
+        InterpretedFunctionTests.bpl(2,3): anon0
 InterpretedFunctionTests.bpl(10,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    InterpretedFunctionTests.bpl(8,3): anon0
+        InterpretedFunctionTests.bpl(8,3): anon0
 InterpretedFunctionTests.bpl(16,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    InterpretedFunctionTests.bpl(14,3): anon0
+        InterpretedFunctionTests.bpl(14,3): anon0
 
 Boogie program verifier finished with 0 verified, 3 errors
-- 
cgit v1.2.3