From f14dcef0d8c0459638c81f7a82972055cfd5d4f7 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 24 Sep 2010 01:11:16 +0000
Subject: Boogie: * Added Test/textbook/DivMod.bpl, which embodies a conversion
 between C's div/mod operators and SMT Lib's div/mod operators. * Added a
 rudimentary printing of variables for captured states.  It doesn't attempt to
 print everything at this time, and it doesn't work when variables get
 unique-ified by @@-suffixes.  A more complete implementation will be added at
 a later time.

---
 Test/test15/Answer | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

(limited to 'Test/test15')

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 969bbe41..825df64f 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -200,8 +200,36 @@ Execution trace:
     CaptureState.bpl(24,5): anon3
 Captured states:
     top
+        Heap = *8
+        F = *10
+        this = *9
+        x = x
+        y = y
+        r = r
+        m = -2
     then
+        Heap = *8
+        F = *10
+        this = *9
+        x = x
+        y = y
+        r = r
+        m = -1
     postUpdate0
+        Heap = *8
+        F = *10
+        this = *9
+        x = x
+        y = y
+        r = r
+        m = -1
     end
+        Heap = *8
+        F = *10
+        this = *9
+        x = x
+        y = y
+        r = -2
+        m = -1
 
 Boogie program verifier finished with 0 verified, 1 error
-- 
cgit v1.2.3