summaryrefslogtreecommitdiff
path: root/Test/datatypes/Answer
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-03-05 15:42:12 -0800
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-03-05 15:42:12 -0800
commit47ac92a139c1cc11ff7f68b726960fcd902e41d2 (patch)
tree2cf5bbb30998c8f3987020196c82d94573f1a870 /Test/datatypes/Answer
parentf82dab21f1240fb3f8d67a880f4f93017d85c345 (diff)
fixed datatype bug reported by Chris
fixed function body referring to globals bug
Diffstat (limited to 'Test/datatypes/Answer')
-rw-r--r--Test/datatypes/Answer4
1 files changed, 4 insertions, 0 deletions
diff --git a/Test/datatypes/Answer b/Test/datatypes/Answer
index 7b7b411a..bac8f345 100644
--- a/Test/datatypes/Answer
+++ b/Test/datatypes/Answer
@@ -12,3 +12,7 @@ Execution trace:
t2.bpl(16,3): anon0
Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- ex.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors