From c6d160193cba277905946f27c0dca2bdadb4a919 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Sun, 23 Aug 2015 00:20:16 -0700
Subject: Added /autoTriggers to two tests where it only makes a cosmetic
 difference

---
 Test/dafny0/AutoReq.dfy         | 7 ++++++-
 Test/dafny0/AutoReq.dfy.expect  | 9 ++++++++-
 Test/dafny0/Inverses.dfy        | 5 ++++-
 Test/dafny0/Inverses.dfy.expect | 2 ++
 4 files changed, 20 insertions(+), 3 deletions(-)

(limited to 'Test/dafny0')

diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy
index acfe6b8d..d7c87e6d 100644
--- a/Test/dafny0/AutoReq.dfy
+++ b/Test/dafny0/AutoReq.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function f(x:int) : bool
@@ -313,3 +313,8 @@ module OpaqueTest {
   }
 
 }
+
+// autoTriggers added because it causes an extra error message related to
+// violated preconditions to appear. That extra message is due to the extra
+// precondition involving a split quantifier: the user now gets two traces, one
+// for each conjunct.
diff --git a/Test/dafny0/AutoReq.dfy.expect b/Test/dafny0/AutoReq.dfy.expect
index b4b34e14..25f00797 100644
--- a/Test/dafny0/AutoReq.dfy.expect
+++ b/Test/dafny0/AutoReq.dfy.expect
@@ -1,5 +1,12 @@
 AutoReq.dfy(247,4): Error: possible violation of function precondition
 AutoReq.dfy(239,13): Related location
+AutoReq.dfy(239,59): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon4_Else
+AutoReq.dfy(247,4): Error: possible violation of function precondition
+AutoReq.dfy(239,13): Related location
+AutoReq.dfy(239,35): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon4_Else
@@ -42,4 +49,4 @@ Execution trace:
     (0,0): anon0
     (0,0): anon11_Then
 
-Dafny program verifier finished with 52 verified, 8 errors
+Dafny program verifier finished with 52 verified, 9 errors
diff --git a/Test/dafny0/Inverses.dfy b/Test/dafny0/Inverses.dfy
index 7995255a..b424cfd9 100644
--- a/Test/dafny0/Inverses.dfy
+++ b/Test/dafny0/Inverses.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This identity function is used to so that if the occurrence of i below
@@ -110,3 +110,6 @@ method RotateD<T>(a: array<T>) returns (r: array<T>)
     r[if a.Length - 1 == i then 0 else i + 1] := a[Id(i)];  // yes, Dafny can invert this one
   }
 }
+
+// autoTriggers added because it causes a slight rephrasing of an error
+// message.
diff --git a/Test/dafny0/Inverses.dfy.expect b/Test/dafny0/Inverses.dfy.expect
index 29c67e5d..b9530e3f 100644
--- a/Test/dafny0/Inverses.dfy.expect
+++ b/Test/dafny0/Inverses.dfy.expect
@@ -1,10 +1,12 @@
 Inverses.dfy(70,0): Error BP5003: A postcondition might not hold on this return path.
 Inverses.dfy(69,10): Related location: This is the postcondition that might not hold.
+Inverses.dfy(69,66): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon6_Else
 Inverses.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.
 Inverses.dfy(82,10): Related location: This is the postcondition that might not hold.
+Inverses.dfy(82,66): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon9_Else
-- 
cgit v1.2.3