From a4729bac8fd4a4df88e539f187d1ec4984bec471 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Mon, 2 Jul 2012 11:51:44 -0700
Subject: Dafny: reinstated autocontracts

---
 Source/Dafny/Dafny.atg | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'Source/Dafny/Dafny.atg')

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index bfce5122..7d49fb8f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -778,7 +778,11 @@ UpdateStmt<out Statement/*!*/ s>
   (. if (suchThat != null) {
        s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
      } else {
-       s = new UpdateStmt(x, lhss, rhss);
+       if (lhss.Count == 0 && rhss.Count == 0) {
+         s = new BlockStmt(x, new List<Statement>()); // error, give empty statement
+       } else {
+         s = new UpdateStmt(x, lhss, rhss);
+       }
      }
   .)
   .
-- 
cgit v1.2.3