From b32f277e00ed5c3f90d01c17bcce0d8855eadfff Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Tue, 14 Sep 2010 20:09:39 +0000
Subject: Dafny: * Added internal support for multi-dimensional arrays (but not
 all surface syntax is there yet) * Removed unused variables from Dafny.atg

Boogie and Dafny:
* Improved error message for postcondition violations
---
 Test/codeexpr/Answer | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Test/codeexpr')

diff --git a/Test/codeexpr/Answer b/Test/codeexpr/Answer
index 55709034..9c22ca61 100644
--- a/Test/codeexpr/Answer
+++ b/Test/codeexpr/Answer
@@ -13,7 +13,7 @@ Execution trace:
 Boogie program verifier finished with 3 verified, 3 errors
 
 ------------------------------ CodeExpr1.bpl ---------------------
-CodeExpr1.bpl(44,5): Error BP5003: A postcondition might not hold at this return statement.
+CodeExpr1.bpl(44,5): Error BP5003: A postcondition might not hold on this return path.
 CodeExpr1.bpl(40,3): Related location: This is the postcondition that might not hold.
 Execution trace:
         CodeExpr1.bpl(42,3): start
-- 
cgit v1.2.3