Fix issue 136. Less aggressive Lit wrap for assert/assume.

9 files changed, 18 insertions, 18 deletions

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index 9e36e64c..9891c040 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /compile:0 /autoTriggers:1 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 class C {

diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect
index d32cd9bb..bf7388cf 100644
--- a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect
@@ -1,6 +1,6 @@
 Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> DoNothingToAssert

-Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false);

+Processing command (at Snapshots0.v0.dfy(4,10)) assert false;

   >>> DoNothingToAssert

 

 Dafny program verifier finished with 3 verified, 0 errors

@@ -16,7 +16,7 @@ Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f
   >>> MarkAsFullyVerified

 Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap);

   >>> AssumeNegationOfAssumptionVariable

-Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);

+Processing command (at Snapshots0.v1.dfy(4,10)) assert false;

   >>> MarkAsPartiallyVerified

 Snapshots0.v1.dfy(4,9): Error: assertion violation

 Execution trace:

diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect
index 6d5e43f8..1b5c8d24 100644
--- a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect
@@ -1,6 +1,6 @@
 Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> DoNothingToAssert

-Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false);

+Processing command (at Snapshots1.v0.dfy(4,10)) assert false;

   >>> DoNothingToAssert

 Processing command (at Snapshots1.v0.dfy(12,3)) assert true;

   >>> DoNothingToAssert

@@ -12,7 +12,7 @@ Processing command (at Snapshots1.v1.dfy(12,3)) assert true;
   >>> MarkAsFullyVerified

 Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> MarkAsFullyVerified

-Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false);

+Processing command (at Snapshots1.v1.dfy(4,10)) assert false;

   >>> DoNothingToAssert

 Snapshots1.v1.dfy(4,9): Error: assertion violation

 Execution trace:

diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect
index ee2ceecd..949ecec9 100644
--- a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect
@@ -1,6 +1,6 @@
 Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> DoNothingToAssert

-Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);

+Processing command (at Snapshots2.v0.dfy(4,10)) assert false;

   >>> DoNothingToAssert

 Processing command (at Snapshots2.v0.dfy(11,11)) assert true;

   >>> DoNothingToAssert

@@ -24,7 +24,7 @@ Processing command (at Snapshots2.v1.dfy(18,3)) assert true;
   >>> MarkAsFullyVerified

 Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> MarkAsFullyVerified

-Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false);

+Processing command (at Snapshots2.v1.dfy(4,10)) assert false;

   >>> DoNothingToAssert

 Snapshots2.v1.dfy(4,9): Error: assertion violation

 Execution trace:

diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect
index accacd90..a7f05a68 100644
--- a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect
@@ -1,4 +1,4 @@
-Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0);

+Processing command (at Snapshots3.v0.dfy(9,14)) assert 0 != 0;

   >>> DoNothingToAssert

 Snapshots3.v0.dfy(9,13): Error: assertion violation

 Execution trace:

@@ -6,9 +6,9 @@ Execution trace:
     (0,0): anon3_Else

 

 Dafny program verifier finished with 1 verified, 1 error

-Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true);

+Processing command (at Snapshots3.v1.dfy(5,12)) assert true;

   >>> DoNothingToAssert

-Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0);

+Processing command (at Snapshots3.v1.dfy(9,14)) assert 0 != 0;

   >>> RecycleError

 Snapshots3.v0.dfy(9,13): Error: assertion violation

 Execution trace:

diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect
index d56eb9d0..e0f07849 100644
--- a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect
@@ -2,11 +2,11 @@ Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0);
   >>> DoNothingToAssert

 

 Dafny program verifier finished with 2 verified, 0 errors

-Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1);

+Processing command (at Snapshots4.v1.dfy(5,14)) assert 1 != 1;

   >>> DoNothingToAssert

 Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0);

   >>> MarkAsFullyVerified

-Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2);

+Processing command (at Snapshots4.v1.dfy(10,14)) assert 2 != 2;

   >>> DoNothingToAssert

 Snapshots4.v1.dfy(5,13): Error: assertion violation

 Execution trace:

diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect
index bef5a87d..cdb942bb 100644
--- a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect
@@ -1,8 +1,8 @@
-Processing command (at Snapshots6.v0.dfy(20,14)) assert Lit(false);

+Processing command (at Snapshots6.v0.dfy(20,14)) assert false;

   >>> DoNothingToAssert

 

 Dafny program verifier finished with 4 verified, 0 errors

-Processing command (at Snapshots6.v1.dfy(20,14)) assert Lit(false);

+Processing command (at Snapshots6.v1.dfy(20,14)) assert false;

   >>> DoNothingToAssert

 Snapshots6.v1.dfy(20,13): Error: assertion violation

 Execution trace:

diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect
index b90a6034..a08b32c6 100644
--- a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect
@@ -1,4 +1,4 @@
-Processing command (at Snapshots7.v0.dfy(19,14)) assert Lit(false);

+Processing command (at Snapshots7.v0.dfy(19,14)) assert false;

   >>> DoNothingToAssert

 

 Dafny program verifier finished with 4 verified, 0 errors

@@ -22,7 +22,7 @@ Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##ext
   >>> AssumeNegationOfAssumptionVariable

 Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##4();

   >>> AssumeNegationOfAssumptionVariable

-Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false);

+Processing command (at Snapshots7.v1.dfy(19,14)) assert false;

   >>> MarkAsPartiallyVerified

 Snapshots7.v1.dfy(19,13): Error: assertion violation

 Execution trace:

diff --git a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect
index 625b71b4..e1cbdbe0 100644
--- a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect
@@ -20,7 +20,7 @@ Snapshots8.v0.dfy(13,12): Related location: This is the postcondition that might
 Processing command (at Snapshots8.v0.dfy(23,12)) assert u#0 != 53;

   >>> DoNothingToAssert

 Snapshots8.v0.dfy(23,11): Error: assertion violation

-Processing command (at Snapshots8.v0.dfy(28,10)) assert Lit(true);

+Processing command (at Snapshots8.v0.dfy(28,10)) assert true;

   >>> DoNothingToAssert

 

 Dafny program verifier finished with 7 verified, 4 errors

@@ -45,7 +45,7 @@ Snapshots8.v1.dfy(12,20): Related location: This is the precondition that might
 Snapshots8.v1.dfy(7,11): Error: assertion violation

 Processing command (at Snapshots8.v1.dfy(21,12)) assert true;

   >>> MarkAsFullyVerified

-Processing command (at Snapshots8.v1.dfy(23,12)) assert Lit(true);

+Processing command (at Snapshots8.v1.dfy(23,12)) assert true;

   >>> DoNothingToAssert

 Processing command (at Snapshots8.v1.dfy(19,13)) assert LitInt(2) <= z#0;

   >>> DoNothingToAssert