From 13a88d7263c02590f5be9bb9944c0ab43b76bccc Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Fri, 26 Feb 2016 09:56:59 -0800
Subject: Fix issue 136. Less aggressive Lit wrap for assert/assume.

---
 Test/dafny0/DTypes.dfy                          | 2 +-
 Test/dafny0/snapshots/Snapshots0.run.dfy.expect | 4 ++--
 Test/dafny0/snapshots/Snapshots1.run.dfy.expect | 4 ++--
 Test/dafny0/snapshots/Snapshots2.run.dfy.expect | 4 ++--
 Test/dafny0/snapshots/Snapshots3.run.dfy.expect | 6 +++---
 Test/dafny0/snapshots/Snapshots4.run.dfy.expect | 4 ++--
 Test/dafny0/snapshots/Snapshots6.run.dfy.expect | 4 ++--
 Test/dafny0/snapshots/Snapshots7.run.dfy.expect | 4 ++--
 Test/dafny0/snapshots/Snapshots8.run.dfy.expect | 4 ++--
 9 files changed, 18 insertions(+), 18 deletions(-)

(limited to 'Test/dafny0')

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
-- 
cgit v1.2.3