Added /autoTriggers to two tests where it only makes a cosmetic difference

4 files changed, 20 insertions, 3 deletions

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