Added tests: parallel calc, better well-formedness checks, calc expression.

2 files changed, 19 insertions, 3 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index a5c48e9a..c738f058 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1795,12 +1795,12 @@ Calculations.dfy(8,17): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon13_Then

-Calculations.dfy(36,11): Error: assertion violation

+Calculations.dfy(42,11): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    Calculations.dfy(31,2): anon5_Else

+    Calculations.dfy(37,2): anon5_Else

 

-Dafny program verifier finished with 4 verified, 4 errors

+Dafny program verifier finished with 5 verified, 4 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 80775896..aa447d9f 100644
--- a/Test/dafny0/Calculations.dfy
+++ b/Test/dafny0/Calculations.dfy
@@ -16,6 +16,12 @@ method CalcTest0(s: seq<int>) {
 			s[0];
 		}
 	}
+	assume forall x :: x in s ==> x >= 0;
+	calc ==> {
+		0 < |s|;
+		{ assert s[0] >= 0; } // OK: well-formed after previous line
+		s[0] >= 0; // OK: well-formed after previous line
+	}
 }
 
 method CalcTest1(x: int, y: int) {
@@ -34,4 +40,14 @@ method CalcTest2(x: int, y: int) {
 		y + x;
 	}
 	assert x == 0; // error: even though assumed above, is not exported by the calculation
+}
+
+// calc expression:
+function CalcTest(s: seq<int>): int {
+	calc < {
+		0;
+		{ assume |s| == 5; }
+		|s|;
+	}
+	s[0]
 }
\ No newline at end of file