From e7534575867b8439af0ce747ea14e32f222cec92 Mon Sep 17 00:00:00 2001
From: stefanheule <unknown>
Date: Tue, 13 Mar 2012 04:45:51 -0700
Subject: Chalice: Do not print empty conditionals.

---
 Chalice/src/main/scala/Boogie.scala | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/Chalice/src/main/scala/Boogie.scala b/Chalice/src/main/scala/Boogie.scala
index acc061ad..900ad6d1 100644
--- a/Chalice/src/main/scala/Boogie.scala
+++ b/Chalice/src/main/scala/Boogie.scala
@@ -222,13 +222,17 @@ object Boogie {
      indent +  "assert " + "{:msg \"" + pos + assert.message + "\"}" + (assert.subsumption match {case Some(n) => "{:subsumption " + n + "}"; case None => ""}) + " " + PrintExpr(e) + ";" + nl
    case Assume(e) => indent + "assume " + PrintExpr(e) +  ";" + nl
    case If(guard, thn, els) =>
+     if (thn == Nil && els == Nil) "" else
      indent + "if (" +
      (if (guard == null) "*" else PrintExpr(guard)) +
      ") {" +  nl + 
      IndentMore { Print(thn, "", PrintStmt)  } + 
-     indent +  "} else {"  + nl + 
-     IndentMore { Print(els, "", PrintStmt)  } + 
-     indent + "}" + nl
+     indent +  "}" +
+     (if (els == Nil) nl else
+       " else {"  + nl + 
+       IndentMore { Print(els, "", PrintStmt)  } + 
+       indent + "}" + nl
+     )
    case Assign(lhs, rhs) =>
      indent + PrintExpr(lhs) + " := " + PrintExpr(rhs) + ";" + nl
    case AssignMap(lhs, index, rhs) =>
-- 
cgit v1.2.3