From b8fad094ad74180ca16670bebe602737d856b5da Mon Sep 17 00:00:00 2001 From: qunyanm Date: Wed, 25 Nov 2015 10:27:02 -0800 Subject: Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that the auto-triggers can be computed for ForallStmt. --- Test/dafny0/SmallTests.dfy.expect | 1 + 1 file changed, 1 insertion(+) (limited to 'Test/dafny0') diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index 4bd12096..6161c3dd 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -1,3 +1,4 @@ +SmallTests.dfy(507,4): Warning: /!\ No trigger covering all quantified variables found. SmallTests.dfy(34,10): Error: index out of range Execution trace: (0,0): anon0 -- cgit v1.2.3