Allowing dangling hints in calculations.

2 files changed, 29 insertions, 2 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 38b7c120..769c66ca 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1685,8 +1685,16 @@ Calculations.dfy(52,11): Error: assertion violation
 Execution trace:

     (0,0): anon0

     Calculations.dfy(47,2): anon5_Else

+Calculations.dfy(75,13): Error: index out of range

+Execution trace:

+    (0,0): anon0

+    (0,0): anon12_Then

+Calculations.dfy(75,17): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon12_Then

 

-Dafny program verifier finished with 5 verified, 4 errors

+Dafny program verifier finished with 6 verified, 6 errors

 

 -------------------- IteratorResolution.dfy --------------------

 IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field

diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
index 54a9a3d4..59191ac3 100644
--- a/Test/dafny0/Calculations.dfy
+++ b/Test/dafny0/Calculations.dfy
@@ -60,4 +60,23 @@ function CalcTest3(s: seq<int>): int {
 		|s|;
 	}
 	s[0]
-}
\ No newline at end of file
+}
+
+// dangling hints:
+method CalcTest4(s: seq<int>) 
+	requires forall n | n in s :: n > 0;
+{
+	calc {
+		1 + 1;
+		{ assert 1 + 1 == 2; }
+	}
+	calc {
+		2;
+		{ assert s[0] > 0; } // error: ill-formed hint
+	}
+	calc {
+		|s| > 0;
+	==> { assert s[0] > 0; } // okay
+	}
+	
+}