From 26bdec533c18c1f9afdae9cf67bb18db8ce94199 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Tue, 24 Jan 2012 16:41:59 +0100
Subject: Dafny: Fixed a bug in the printing of let expressions.

---
 Source/Dafny/Printer.cs |  1 +
 Test/dafny0/Answer      | 20 ++++++++++++++++++++
 Test/dafny0/LetExpr.dfy |  2 +-
 Test/dafny0/runtest.bat |  2 +-
 4 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index f98f7cbe..9bd29da0 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1080,6 +1080,7 @@ namespace Microsoft.Dafny {
         var e = (LetExpr)expr;
         bool parensNeeded = !isRightmost;
         if (parensNeeded) { wr.Write("("); }
+        wr.Write("var ");
         string sep = "";
         foreach (var v in e.Vars) {
           wr.Write("{0}{1}", sep, v.Name);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 7baa5817..6f160a66 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1674,3 +1674,23 @@ Execution trace:
     (0,0): anon6_Else
 
 Dafny program verifier finished with 58 verified, 21 errors
+
+-------------------- LetExpr.dfy --------------------
+LetExpr.dfy(5,12): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+LetExpr.dfy(104,21): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon11_Then
+
+Dafny program verifier finished with 13 verified, 2 errors
+out.tmp.dfy(10,12): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+out.tmp.dfy(101,21): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon11_Then
+
+Dafny program verifier finished with 13 verified, 2 errors
diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy
index 703813d2..48e4810b 100644
--- a/Test/dafny0/LetExpr.dfy
+++ b/Test/dafny0/LetExpr.dfy
@@ -1,5 +1,5 @@
 method M0(n: int)
-  requires var f := 100; n < f;
+  requires var f := 100; n < f; requires var t, f := true, false; (t && f) || n < 100;
 {
   assert n < 200;
   assert 0 <= n;  // error
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 0da3b411..d09e1cc2 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -27,7 +27,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
 )
 
-for %%f in (SmallTests.dfy) do (
+for %%f in (SmallTests.dfy LetExpr.dfy) do (
   echo.
   echo -------------------- %%f --------------------
   %DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f
-- 
cgit v1.2.3