From db36523d7f468381dad680fdcf02f0db54a20007 Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Wed, 30 Nov 2011 20:07:57 -0800
Subject: a bug fix in model parsing

---
 Source/Model/Model.cs | 16 +++++-----------
 1 file changed, 5 insertions(+), 11 deletions(-)

(limited to 'Source/Model')

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 07a0af3e..0b20ff33 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -847,17 +847,11 @@ namespace Microsoft.Boogie
                 if (tuple.Count == 0) continue;
                 string tuple0 = tuple[0] as string;
                 if (tuple.Count == 1) {
-                  if (fn != null) {
-                    if (tuple0 != "}") BadModel("invalid function tuple definition");
-                    break;
-                  }
-                  else {
-                    fn = currModel.TryGetFunc(funName);
-                    if (fn == null)
-                      fn = currModel.MkFunc(funName, 1);
-                    fn.Else = GetElt(tuple0);
-                    continue;
-                  }
+                  if (fn == null)
+                    fn = currModel.MkFunc(funName, 1);
+                  if (tuple0 == "}") break;
+                  fn.Else = GetElt(tuple0);
+                  continue;
                 }
                 string tuplePenultimate = tuple[tuple.Count - 2] as string;
                 if (tuplePenultimate != "->") BadModel("invalid function tuple definition");
-- 
cgit v1.2.3