From d4d59ba1cbc91160a3d15cbf615878af971448e6 Mon Sep 17 00:00:00 2001
From: Ken McMillan <unknown>
Date: Fri, 21 Feb 2014 12:13:20 -0800
Subject: Fixed crash in ModelParser when Z3 returns an operator that is a
 list.

---
 Source/Model/ModelParser.cs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'Source')

diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs
index dc6e06b5..ded145ed 100644
--- a/Source/Model/ModelParser.cs
+++ b/Source/Model/ModelParser.cs
@@ -65,7 +65,9 @@ namespace Microsoft.Boogie
 			string s = o as string;
 			if (s != null)
 				return GetElt (s);
-			List<object> os = (List<object>)o;
+			List<object> os = (List<object>)o;
+            if (!(os[0] is string))
+                os.Insert(0, "_");  // KLM: fix crash on ((as const (Array Int Int)) 0)
 			List<Model.Element> args = new List<Model.Element> ();
 			for (int i = 1; i < os.Count; i++) {
 				args.Add (GetElt (os [i]));
-- 
cgit v1.2.3