From 13d181a688ef5a5f1acd72928f7bef12d146ebad Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Tue, 21 Oct 2014 18:28:42 -0700
Subject: When guessing decreases clauses for loops, convert numeric values to
 their ultimate base type (int or real) before subtracting

---
 Test/dafny0/Newtypes.dfy.expect | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'Test/dafny0/Newtypes.dfy.expect')

diff --git a/Test/dafny0/Newtypes.dfy.expect b/Test/dafny0/Newtypes.dfy.expect
index 7af53142..3ca77f1d 100644
--- a/Test/dafny0/Newtypes.dfy.expect
+++ b/Test/dafny0/Newtypes.dfy.expect
@@ -42,5 +42,17 @@ Newtypes.dfy(225,40): Error: result of operation might violate newtype constrain
 Execution trace:
     (0,0): anon0
     (0,0): anon8_Then
+Newtypes.dfy(237,19): Error: result of operation might violate newtype constraint
+Execution trace:
+    (0,0): anon0
+    Newtypes.dfy(236,5): anon9_LoopHead
+    (0,0): anon9_LoopBody
+    (0,0): anon10_Then
+Newtypes.dfy(277,19): Error: result of operation might violate newtype constraint
+Execution trace:
+    (0,0): anon0
+    Newtypes.dfy(276,5): anon9_LoopHead
+    (0,0): anon9_LoopBody
+    (0,0): anon10_Then
 
-Dafny program verifier finished with 35 verified, 11 errors
+Dafny program verifier finished with 47 verified, 13 errors
-- 
cgit v1.2.3