refactoring and fixes in the SMTLIB2 parser

1 files changed, 273 insertions, 309 deletions

diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs
index 40fd3c9a..ed9ea2f4 100644
--- a/Source/Model/ModelParser.cs
+++ b/Source/Model/ModelParser.cs
@@ -16,27 +16,27 @@ namespace Microsoft.Boogie
 	{
 		protected Model currModel;
 		int lineNo;
-		internal List<Model> resModels = new List<Model> ();
+		internal List<Model> resModels = new List<Model>();
 		internal System.IO.TextReader rd;
 		string lastLine = "";
 		protected static char[] seps = new char[] { ' ' };
-		protected static Regex bv = new Regex (@"\(_ BitVec (\d+)\)");
+		protected static Regex bv = new Regex(@"\(_ BitVec (\d+)\)");
 
-		protected void NewModel ()
+		protected void NewModel()
 		{
 			lastLine = "";
-			currModel = new Model ();
-			resModels.Add (currModel);
+			currModel = new Model();
+			resModels.Add(currModel);
 		}
 
-		protected void BadModel (string msg)
+		protected void BadModel(string msg)
 		{
-			throw new ArgumentException (string.Format ("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine));
+			throw new ArgumentException(string.Format("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine));
 		}
 
-		protected string ReadLine ()
+		protected string ReadLine()
 		{
-			var l = rd.ReadLine ();
+			var l = rd.ReadLine();
 			if (l != null) {
 				lineNo++;
 				lastLine = l;
@@ -44,36 +44,36 @@ namespace Microsoft.Boogie
 			return l;
 		}
 
-		string[] GetWords (string line)
+		string[] GetWords(string line)
 		{
 			if (line == null)
 				return null;
-			var words = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+			var words = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
 			return words;
 		}
 
-		Model.Element GetElt (string name)
+		Model.Element GetElt(string name)
 		{
-			Model.Element ret = currModel.TryMkElement (name);
+			Model.Element ret = currModel.TryMkElement(name);
 			if (ret == null)
-				BadModel ("invalid element name " + name);
+				BadModel("invalid element name " + name);
 			return ret;
 		}
 
-		protected Model.Element GetElt (object o)
+		protected Model.Element GetElt(object o)
 		{
 			string s = o as string;
 			if (s != null)
-				return GetElt (s);
+				return GetElt(s);
 			List<object> os = (List<object>)o;
-			List<Model.Element> args = new List<Model.Element> ();
+			List<Model.Element> args = new List<Model.Element>();
 			for (int i = 1; i < os.Count; i++) {
-				args.Add (GetElt (os [i]));
+				args.Add(GetElt(os[i]));
 			}
-			return new Model.DatatypeValue (currModel, (string)os [0], args);
+			return new Model.DatatypeValue(currModel, (string)os[0], args);
 		}
 
-		protected int CountOpenParentheses (string s, int n)
+		protected int CountOpenParentheses(string s, int n)
 		{
 			int f = n;
 			foreach (char c in s) {
@@ -83,174 +83,174 @@ namespace Microsoft.Boogie
 					f--;
 			}
 			if (f < 0)
-				BadModel ("mismatched parentheses in datatype term");
+				BadModel("mismatched parentheses in datatype term");
 			return f;
 		}
 
-		abstract internal void Run ();
+		abstract internal void Run();
 	}
 
 	class ParserZ3 : ModelParser
 	{
-		List<object> GetFunctionTokens (string newLine)
+		List<object> GetFunctionTokens(string newLine)
 		{
 			if (newLine == null)
 				return null;
-			newLine = bv.Replace (newLine, "bv${1}");
+			newLine = bv.Replace(newLine, "bv${1}");
 			string line = newLine;
-			int openParenCounter = CountOpenParentheses (newLine, 0);
-			if (!newLine.Contains ("}")) {
+			int openParenCounter = CountOpenParentheses(newLine, 0);
+			if (!newLine.Contains("}")) {
 				while (openParenCounter > 0) {
-					newLine = ReadLine ();
+					newLine = ReadLine();
 					if (newLine == null) {
 						return null;
 					}
 					line += newLine;
-					openParenCounter = CountOpenParentheses (newLine, openParenCounter);
+					openParenCounter = CountOpenParentheses(newLine, openParenCounter);
 				}
 			}
 
-			line = line.Replace ("(", " ( ");
-			line = line.Replace (")", " ) ");
-			var tuple = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+			line = line.Replace("(", " ( ");
+			line = line.Replace(")", " ) ");
+			var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
 
-			List<object> newTuple = new List<object> ();
-			Stack<List<object>> wordStack = new Stack<List<object>> ();
+			List<object> newTuple = new List<object>();
+			Stack<List<object>> wordStack = new Stack<List<object>>();
 			for (int i = 0; i < tuple.Length; i++) {
-				string elem = tuple [i];
+				string elem = tuple[i];
 				if (elem == "(") {
-					List<object> ls = new List<object> ();
-					wordStack.Push (ls);
+					List<object> ls = new List<object>();
+					wordStack.Push(ls);
 				} else if (elem == ")") {
-					List<object> ls = wordStack.Pop ();
+					List<object> ls = wordStack.Pop();
 					if (wordStack.Count > 0) {
-						wordStack.Peek ().Add (ls);
+						wordStack.Peek().Add(ls);
 					} else {
-						newTuple.Add (ls);
+						newTuple.Add(ls);
 					}
 				} else if (wordStack.Count > 0) {
-					wordStack.Peek ().Add (elem);
+					wordStack.Peek().Add(elem);
 				} else {
-					newTuple.Add (elem);
+					newTuple.Add(elem);
 				}
 			}
 			return newTuple;
 		}
 
-		internal override void Run ()
+		internal override void Run()
 		{
-			var selectFunctions = new Dictionary<int, Model.Func> ();
-			var storeFunctions = new Dictionary<int, Model.Func> ();
+			var selectFunctions = new Dictionary<int, Model.Func>();
+			var storeFunctions = new Dictionary<int, Model.Func>();
 			for (; ;) {
-				var line = ReadLine ();
+				var line = ReadLine();
 				if (line == null)
 					break; // end of model, everything fine
 
 				if (line == "Counterexample:" || line == "Error model: " || line == "*** MODEL") {
-					NewModel ();
+					NewModel();
 					continue;
 				}
 
-				if (line.EndsWith (": Invalid.") || line.EndsWith (": Valid.") || line.StartsWith ("labels:"))
+				if (line.EndsWith(": Invalid.") || line.EndsWith(": Valid.") || line.StartsWith("labels:"))
 					continue;
 				if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")
 					continue;
 
-				var words = GetFunctionTokens (line);
+				var words = GetFunctionTokens(line);
 				if (words.Count == 0)
 					continue;
-				var lastWord = words [words.Count - 1];
+				var lastWord = words[words.Count - 1];
 
 				if (currModel == null)
-					BadModel ("model begin marker not found");
+					BadModel("model begin marker not found");
 
-				if (line.StartsWith ("*** STATE ")) {
-					var name = line.Substring (10);
+				if (line.StartsWith("*** STATE ")) {
+					var name = line.Substring(10);
 					Model.CapturedState cs;
 					if (name == "<initial>")
 						cs = currModel.InitialState;
 					else
-						cs = currModel.MkState (name);
+						cs = currModel.MkState(name);
 					for (; ;) {
-						var tmpline = ReadLine ();
+						var tmpline = ReadLine();
 						if (tmpline == "*** END_STATE")
 							break;
-						var tuple = GetFunctionTokens (tmpline);
+						var tuple = GetFunctionTokens(tmpline);
 						if (tuple == null)
-							BadModel ("EOF in state table");
+							BadModel("EOF in state table");
 						if (tuple.Count == 0)
 							continue;
-						if (tuple.Count == 3 && tuple [0] is string && tuple [1] is string && ((string)tuple [1]) == "->") {
-							cs.AddBinding ((string)tuple [0], GetElt (tuple [2]));
+						if (tuple.Count == 3 && tuple[0] is string && tuple[1] is string && ((string)tuple[1]) == "->") {
+							cs.AddBinding((string)tuple[0], GetElt(tuple[2]));
 						} else {
-							BadModel ("invalid state tuple definition");
+							BadModel("invalid state tuple definition");
 						}
 					}
 					continue;
 				}
 
-				if (words.Count == 3 && words [1] is string && ((string)words [1]) == "->") {
-					var funName = (string)words [0];
+				if (words.Count == 3 && words[1] is string && ((string)words[1]) == "->") {
+					var funName = (string)words[0];
 					Model.Func fn = null;
 
 					if (lastWord is string && ((string)lastWord) == "{") {
-						fn = currModel.TryGetFunc (funName);
+						fn = currModel.TryGetFunc(funName);
 						for (; ;) {
-							var tuple = GetFunctionTokens (ReadLine ());
+							var tuple = GetFunctionTokens(ReadLine());
 							if (tuple == null)
-								BadModel ("EOF in function table");
+								BadModel("EOF in function table");
 							if (tuple.Count == 0)
 								continue;
-							string tuple0 = tuple [0] as string;
+							string tuple0 = tuple[0] as string;
 							if (tuple.Count == 1) {
 								if (fn == null)
-									fn = currModel.MkFunc (funName, 1);
+									fn = currModel.MkFunc(funName, 1);
 								if (tuple0 == "}")
 									break;
 								if (fn.Else == null)
-									fn.Else = GetElt (tuple [0]);
+									fn.Else = GetElt(tuple[0]);
 								continue;
 							}
-							string tuplePenultimate = tuple [tuple.Count - 2] as string;
+							string tuplePenultimate = tuple[tuple.Count - 2] as string;
 							if (tuplePenultimate != "->")
-								BadModel ("invalid function tuple definition");
-							var resultName = tuple [tuple.Count - 1];
+								BadModel("invalid function tuple definition");
+							var resultName = tuple[tuple.Count - 1];
 							if (tuple0 == "else") {
 								if (fn != null && !(resultName is string && ((string)resultName) == "#unspecified") && fn.Else == null) {
-									fn.Else = GetElt (resultName);
+									fn.Else = GetElt(resultName);
 								}
 								continue;
 							}
 
 							if (fn == null) {
 								var arity = tuple.Count - 2;
-								if (Regex.IsMatch (funName, "^MapType[0-9]*Select$")) {
-									funName = string.Format ("[{0}]", arity);
-									if (!selectFunctions.TryGetValue (arity, out fn)) {
-										fn = currModel.MkFunc (funName, arity);
-										selectFunctions.Add (arity, fn);
+								if (Regex.IsMatch(funName, "^MapType[0-9]*Select$")) {
+									funName = string.Format("[{0}]", arity);
+									if (!selectFunctions.TryGetValue(arity, out fn)) {
+										fn = currModel.MkFunc(funName, arity);
+										selectFunctions.Add(arity, fn);
 									}
-								} else if (Regex.IsMatch (funName, "^MapType[0-9]*Store$")) {
-									funName = string.Format ("[{0}:=]", arity);
-									if (!storeFunctions.TryGetValue (arity, out fn)) {
-										fn = currModel.MkFunc (funName, arity);
-										storeFunctions.Add (arity, fn);
+								} else if (Regex.IsMatch(funName, "^MapType[0-9]*Store$")) {
+									funName = string.Format("[{0}:=]", arity);
+									if (!storeFunctions.TryGetValue(arity, out fn)) {
+										fn = currModel.MkFunc(funName, arity);
+										storeFunctions.Add(arity, fn);
 									}
 								} else {
-									fn = currModel.MkFunc (funName, arity);
+									fn = currModel.MkFunc(funName, arity);
 								}
 							}
 							var args = new Model.Element[fn.Arity];
 							for (int i = 0; i < fn.Arity; ++i)
-								args [i] = GetElt (tuple [i]);
-							fn.AddApp (GetElt (resultName), args);
+								args[i] = GetElt(tuple[i]);
+							fn.AddApp(GetElt(resultName), args);
 						}
 					} else {
-						fn = currModel.MkFunc (funName, 0);
-						fn.SetConstant (GetElt (lastWord));
+						fn = currModel.MkFunc(funName, 0);
+						fn.SetConstant(GetElt(lastWord));
 					}
 				} else {
-					BadModel ("unidentified line");
+					BadModel("unidentified line");
 				}
 			}
 		}
@@ -264,7 +264,7 @@ namespace Microsoft.Boogie
 		int arrayNum;
 		int index;
 
-		void FindArity ()
+		void FindArity()
 		{
 			arity = 0;
 			int p_count = 1;
@@ -273,9 +273,9 @@ namespace Microsoft.Boogie
 			while (p_count > 0) {
 				if (i == tokens.Length - 1)
 					break;
-				else if (tokens [i] == ")")
+				else if (tokens[i] == ")")
 					p_count--;
-				else if (tokens [i] == "(" && tokens [i + 1] != "ite") {
+				else if (tokens[i] == "(" && tokens[i + 1] != "ite") {
 					p_count++;
 					arity++;
 				}
@@ -284,159 +284,171 @@ namespace Microsoft.Boogie
 			}
 		}
 
-		string GetValue (int idx)
+		string GetValue(int idx)
 		{
-			string value = tokens [idx];
+			string value = tokens[idx];
 
-			if (tokens [idx - 1] == "-") {
+			if (tokens[idx - 1] == "-") {
 				value = "(- " + value + ")";
-			} else if (tokens [idx - 2] == "_") {
-				value = tokens [idx - 1] + "[" + tokens [idx] + "]";
+			} else if (tokens[idx - 2] == "_") {
+				value = tokens[idx - 1] + "[" + tokens[idx] + "]";
 			}
 
 			return value;
 		}
 
-		void SplitArrayExpression ()
+		List<string>[] TrySplitExpr(List<string> expr)
 		{
-			output.Add ("as-array[k!" + arrayNum + "]");
+			int splits = 1;
+			foreach (string tok in expr)
+				if (tok.Equals("@SPLIT"))
+					splits++;
+
+			List<string>[] newExpr = new List<string>[splits];
 
-			if (output.Contains ("@SPLIT")) {
-				output.Add (" ");
-				output.Add ("}");
+			for (int s = 0; s < splits; s++)
+				newExpr[s] = new List<string>();
+
+			int i = 0;
+			foreach (string tok in expr) {
+				if (tok.Equals("@SPLIT")) {
+					i++;
+					continue;
+				}
+
+				newExpr[i].Add(tok);
 			}
 
-			output.Add ("@SPLIT");
-			output.Add ("k!" + arrayNum);
-			output.Add ("->");
-			output.Add ("{");
-			output.Add (" ");
+			return newExpr;
+		}
+
+		void SplitArrayExpression()
+		{
+			output.Add("as-array[k!" + arrayNum + "]");
+
+			if (output.Contains("@SPLIT")) {
+				output.Add(" ");
+				output.Add("}");
+			}
+
+			output.Add("@SPLIT");
+			output.Add("k!" + arrayNum);
+			output.Add("->");
+			output.Add("{");
+			output.Add(" ");
 
 			arrayNum++;
 		}
 
-		void ParseArrayExpr ()
+		void ParseArrayExpr()
 		{
 			while (tokens [index] != "as-array" && tokens [index] != "store" && tokens [index] != "__array_store_all__")
 				index++;
 
-			if (tokens [index] == "store") {
-				SplitArrayExpression ();
+			if (tokens[index] == "store") {
+				SplitArrayExpression();
 
-				List<string> args = new List<string> ();
+				List<string> args = new List<string>();
 				int p_count = 1;
 				index += 4;
 
 				while (p_count > 0) {
-					if (tokens [index] == ")")
+					if (tokens[index] == ")")
 						p_count--;
-					else if (tokens [index] == "(")
+					else if (tokens[index] == "(")
 						p_count++;
 					index++;
 				}
 
-				if ((tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") ||
-				    (tokens [index] == "(" && tokens [index + 1] == "store")) {
-					SplitArrayExpression ();
+				if ((tokens[index] == "(" && tokens[index + 1] == "__array_store_all__") ||
+					(tokens[index] == "(" && tokens[index + 1] == "store")) {
+					SplitArrayExpression();
 				} else {
 					while (args.Count < 3) {
-						if (tokens [index] == ")")
+						if (tokens[index] == ")")
 							index++;
-						else if (tokens [index] == "(") {
+						else if (tokens[index] == "(") {
 							while (tokens [index] != ")")
 								index++;
-							args.Add (GetValue (index - 1));
+							args.Add(GetValue(index - 1));
 						} else {
-							args.Add (GetValue (index));
+							args.Add(GetValue(index));
 						}
 
 						index++;
 					}
 
-					output.Add (args [1]);
-					output.Add ("->");
-					output.Add (args [2]);
-					output.Add (" ");
-					output.Add ("else");
-					output.Add ("->");
-					output.Add (args [0]);
+					output.Add(args[1]);
+					output.Add("->");
+					output.Add(args[2]);
+					output.Add(" ");
+					output.Add("else");
+					output.Add("->");
+					output.Add(args[0]);
 				}
-			} else if (tokens [index] == "__array_store_all__") {
-				SplitArrayExpression ();
+			} else if (tokens[index] == "__array_store_all__") {
+				SplitArrayExpression();
 
 				while (tokens[index] == "__array_store_all__") {
 					int p_count = 1;
 					index += 2;
 
 					while (p_count > 0) {
-						if (tokens [index] == ")")
+						if (tokens[index] == ")")
 							p_count--;
-						else if (tokens [index] == "(")
+						else if (tokens[index] == "(")
 							p_count++;
 						index++;
 					}
 
-					if (tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") {
-						SplitArrayExpression ();
+					if (tokens[index] == "(" && tokens[index + 1] == "__array_store_all__") {
+						SplitArrayExpression();
 						index++;
 					} else {
-						if (tokens [index] == ")")
+						if (tokens[index] == ")")
 							index++;
-						else if (tokens [index] == "(") {
+						else if (tokens[index] == "(") {
 							while (tokens [index] != ")")
 								index++;
-							output.Add (GetValue (index - 1));
+							output.Add(GetValue(index - 1));
 						} else {
-							output.Add (GetValue (index));
+							output.Add(GetValue(index));
 						}
 
 						index++;
 					}
 				}
-			} else if (tokens [index] == "as-array") {
-				output.Add ("as-array[" + tokens [index + 1] + "]");
+			} else if (tokens[index] == "as-array") {
+				output.Add("as-array[" + tokens[index + 1] + "]");
 			}
 		}
 
-		void ParseIteExpr ()
+		void ParseIteExpr()
 		{
-			List<string> args = new List<string> ();
-			List<string> results = new List<string> ();
-
-			FindArity ();
+			List<string> args = new List<string>();
+			List<string> results = new List<string>();
 
-			int occurrences = 0;
-
-			foreach (string tok in tokens) {
-				if (tok == "_ufmt_1")
-					occurrences++;
-			}
+			FindArity();
 
 			for (; ;) {
 				index++;
 
-				if (tokens [index] == "=") {
-					index += 2;
-
-					if (tokens [index] == "(") {
-						while (tokens [index] != ")")
-							index++;
-						args.Add (GetValue (index - 1));
-					} else {
-						args.Add (GetValue (index));
-					}
+				if (tokens[index] == "=") {
+					while (tokens[index] != ")")
+						index++;
+					args.Add(GetValue(index - 1));
 				}
 
-				if ((args.Count > 0 && args.Count % arity == 0) ||
-				    (results.Count > 0 && occurrences <= 2 && occurrences > 0)) {
-					index += 2;
+				if (args.Count > 0 && args.Count % arity == 0) {
+					while (tokens[index] == ")")
+						index++;
 
-					if (tokens [index] == "(") {
-						while (tokens [index] != ")")
+					if (tokens[index] == "(") {
+						while (tokens[index] != ")")
 							index++;
-						results.Add (GetValue (index - 1));
+						results.Add(GetValue(index - 1));
 					} else {
-						results.Add (GetValue (index));
+						results.Add(GetValue(index));
 					}
 
 					while (index < tokens.Length - 1 && tokens[index + 1] != "=")
@@ -445,7 +457,7 @@ namespace Microsoft.Boogie
 					if (index == tokens.Length - 1) {
 						while (tokens[index] == ")")
 							index += -1;
-						results.Add (GetValue (index));
+						results.Add(GetValue(index));
 						break;
 					}
 				}
@@ -454,139 +466,91 @@ namespace Microsoft.Boogie
 			int i = 0;
 
 			for (int j = 0; j < results.Count - 1; j++) {
-				if (occurrences > 2) {
-					for (int r = 0; r < arity; r++) {
-						output.Add (args [i]);
-						i++;
-					}
-				} else if (occurrences > 0) {
-					if (arity == 1) {
-						output.Add (args [i]);
-						i++;
-					} else {
-						output.Add (args [0]);
-
-						for (int r = 1; r < arity; r++) {
-							i++;
-							output.Add (args [i]);
-						}
-					}
-				} else {
-					for (int r = 0; r < arity; r++) {
-						output.Add (args [i]);
-						i++;
-					}
+				for (int r = 0; r < arity; r++) {
+					output.Add(args[i]);
+					i++;
 				}
 
-				output.Add ("->");
-				output.Add (results [j]);
-				output.Add (" ");
+				output.Add("->");
+				output.Add(results[j]);
+				output.Add(" ");
 			}
 
-			output.Add ("else");
-			output.Add ("->");
-			output.Add (results [results.Count - 1]);
+			output.Add("else");
+			output.Add("->");
+			output.Add(results[results.Count - 1]);
 		}
 
-		void ParseEndOfExpr ()
+		void ParseEndOfExpr()
 		{
 			index++;
 
 			if (index == tokens.Length && output.Count == 2) {
 				index += -2;
 
-				if (tokens [index] == ")") {
+				if (tokens[index] == ")") {
 					index += -1;
-					output.Add (GetValue (index));
+					output.Add(GetValue(index));
 				} else {
-					output.Add (GetValue (index));
+					output.Add(GetValue(index));
 				}
 			}
 
-			if (index == tokens.Length && output.Contains ("{")) {
-				output.Add (" ");
-				output.Add ("}");
-			}
-		}
-
-		List<string>[] TrySplitExpr (List<string> expr)
-		{
-			int splits = 1;
-			foreach (string tok in expr)
-				if (tok.Equals ("@SPLIT"))
-					splits++;
-
-			List<string>[] newExpr = new List<string>[splits];
-
-			for (int s = 0; s < splits; s++)
-				newExpr [s] = new List<string> ();
-
-			int i = 0;
-			foreach (string tok in expr) {
-				if (tok.Equals ("@SPLIT")) {
-					i++;
-					continue;
-				}
-
-				newExpr [i].Add (tok);
+			if (index == tokens.Length && output.Contains("{")) {
+				output.Add(" ");
+				output.Add("}");
 			}
-
-			return newExpr;
 		}
 
-		List<string> GetParsedTokens (string newLine)
+		List<string> GetParsedTokens(string newLine)
 		{
 			if (newLine == null)
 				return null;
-
-			newLine = bv.Replace (newLine, "bv${1}");
-
+			newLine = bv.Replace(newLine, "bv${1}");
 			string line = newLine;
-			int openParenCounter = CountOpenParentheses (newLine, 0);
-
+			int openParenCounter = CountOpenParentheses(newLine, 0);
 			while (openParenCounter > 0) {
-				newLine = ReadLine ();
+				newLine = ReadLine();
 				if (newLine == null) {
 					return null;
 				}
 				line += newLine;
-				openParenCounter = CountOpenParentheses (newLine, openParenCounter);
+				openParenCounter = CountOpenParentheses(newLine, openParenCounter);
 			}
 
-			line = line.Replace ("(", " ( ");
-			line = line.Replace (")", " ) ");
+			line = line.Replace("(", " ( ");
+			line = line.Replace(")", " ) ");
 
-			tokens = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
-			output = new List<string> ();
+			tokens = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
+			output = new List<string>();
 
 			index = 0;
 			bool doneParsing = false;
 
 			while (!doneParsing) {
-				switch (tokens [index]) {
+				switch (tokens[index]) {
 				case ")":
-					ParseEndOfExpr ();
+					ParseEndOfExpr();
 					break;
 
 				case "define-fun":
-					output.Add (GetValue (index + 1));
-					output.Add ("->");
+					output.Add(GetValue(index + 1));
+					output.Add("->");
 					index += 2;
 					break;
 
-				case "Array":
-					ParseArrayExpr ();
-					break;
-
-				case "ite":
-					ParseIteExpr ();
-					break;
-
 				case "_ufmt_1":
 				case "x!1":
-					output.Add ("{");
-					output.Add (" ");
-					index++;
+					output.Add("{");
+					output.Add(" ");
+					if (Array.IndexOf(tokens, "ite") > -1)
+					    ParseIteExpr();
+					else
+						index++;
+					break;
+
+				case "Array":
+					ParseArrayExpr();
 					break;
 
 				default:
@@ -601,57 +565,57 @@ namespace Microsoft.Boogie
 			return output;
 		}
 
-		internal override void Run ()
+		internal override void Run()
 		{
-			var selectFunctions = new Dictionary<int, Model.Func> ();
-			var storeFunctions = new Dictionary<int, Model.Func> ();
+			var selectFunctions = new Dictionary<int, Model.Func>();
+			var storeFunctions = new Dictionary<int, Model.Func>();
 			arrayNum = 0;
 
 			for (; ;) {
-				var line = ReadLine ();
+				var line = ReadLine();
 				if (line == null)
 					break; // end of model, everything fine
 				if (line == "Counterexample:" || line == "Error model: " || line == "*** MODEL") {
-					NewModel ();
+					NewModel();
 					continue;
 				}
-				if (line.EndsWith (": Invalid.") || line.EndsWith (": Valid.") || line.StartsWith ("labels:"))
+				if (line.EndsWith(": Invalid.") || line.EndsWith(": Valid.") || line.StartsWith("labels:"))
 					continue;
 				if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")
 					continue;
 
-				//Console.WriteLine("\n\n# :: " + line);
+//				Console.WriteLine("\n\n# :: " + line);
 
-				var words = GetParsedTokens (line);
+				var words = GetParsedTokens(line);
 				if (words.Count == 0)
 					continue;
-				var exprs = TrySplitExpr (words);
+				var exprs = TrySplitExpr(words);
 
 				foreach (List<string> expr in exprs) {
-					/*Console.WriteLine ("");
-					for (int i = 0; i < expr.Count; i++) {
-						Console.Write (expr [i] + " ");
-					}*/
+//					Console.WriteLine ("");
+//					for (int i = 0; i < expr.Count; i++) {
+//						Console.Write (expr [i] + " ");
+//					}
 
-					var lastToken = expr [expr.Count - 1];
+					var lastToken = expr[expr.Count - 1];
 					if (currModel == null)
-						BadModel ("model begin marker not found");
+						BadModel("model begin marker not found");
 
-					if (expr.Count > 3 && expr [1] == "->") {
-						var funName = (string)expr [0];
+					if (expr.Count > 3 && expr[1] == "->") {
+						var funName = (string)expr[0];
 						Model.Func fn = null;
 						int i = 4;
 
-						if (expr [2] != "{" && expr [6] != "{")
-							BadModel ("unidentified function definition 5");
+						if (expr[2] != "{" && expr[6] != "{")
+							BadModel("unidentified function definition 5");
 
-						fn = currModel.TryGetFunc (funName);
+						fn = currModel.TryGetFunc(funName);
 
 						for (; ;) {
-							if (expr [i] == "}") {
+							if (expr[i] == "}") {
 								if (i == expr.Count - 1) {
 									if (fn == null)
-										fn = currModel.MkFunc (funName, 1);
+										fn = currModel.MkFunc(funName, 1);
 									break;
 								} else {
 									i++;
@@ -660,94 +624,94 @@ namespace Microsoft.Boogie
 							}
 
 							for (; ;) {
-								if (expr [i] == " ") {
+								if (expr[i] == " ") {
 									i++;
 									break;
 								}
 
-								if ((i == 4 || i == 8) && expr [i - 1] == " " && expr [i + 1] == " ") {
+								if ((i == 4 || i == 8) && expr[i - 1] == " " && expr[i + 1] == " ") {
 									if (fn.Else == null)
-										fn.Else = GetElt (expr [i]);
+										fn.Else = GetElt(expr[i]);
 									i++;
 									continue;
 								}
 
-								if (expr [i] == "else") {
-									if (expr [i + 1] == "->") {
+								if (expr[i] == "else") {
+									if (expr[i + 1] == "->") {
 										i += 2;
 
-										if (expr [i] == "}")
-											BadModel ("unidentified function definition 1");
+										if (expr[i] == "}")
+											BadModel("unidentified function definition 1");
 
-										if (expr [i] == "{") {
+										if (expr[i] == "{") {
 											i++;
 											continue;
 										} else {
-											if (fn != null && !(expr [i] == "#unspecified") && fn.Else == null)
-												fn.Else = GetElt (expr [i]);
+											if (fn != null && !(expr[i] == "#unspecified") && fn.Else == null)
+												fn.Else = GetElt(expr[i]);
 											i++;
 											continue;
 										}
 									} else
-										BadModel ("unidentified function definition 2");
+										BadModel("unidentified function definition 2");
 								}
 
 								int arity = 0;
 								for (; ;) {
 									arity++;
-									if (expr [arity + i] == " ") {
+									if (expr[arity + i] == " ") {
 										arity -= 2;
 										break;
 									}
 								}
 
-								if (expr [i + arity] == "->") {
+								if (expr[i + arity] == "->") {
 									i += arity + 1;
 
-									if (expr [i] == "}")
-										BadModel ("unidentified function definition 3");
+									if (expr[i] == "}")
+										BadModel("unidentified function definition 3");
 								} else
-									BadModel ("unidentified function definition 4");
+									BadModel("unidentified function definition 4");
 
 								if (fn == null) {
-									if (Regex.IsMatch (funName, "^MapType[0-9]*Select$")) {
-										funName = string.Format ("[{0}]", arity);
+									if (Regex.IsMatch(funName, "^MapType[0-9]*Select$")) {
+										funName = string.Format("[{0}]", arity);
 
-										if (!selectFunctions.TryGetValue (arity, out fn)) {
-											fn = currModel.MkFunc (funName, arity);
-											selectFunctions.Add (arity, fn);
+										if (!selectFunctions.TryGetValue(arity, out fn)) {
+											fn = currModel.MkFunc(funName, arity);
+											selectFunctions.Add(arity, fn);
 										}
-									} else if (Regex.IsMatch (funName, "^MapType[0-9]*Store$")) {
-										funName = string.Format ("[{0}:=]", arity);
+									} else if (Regex.IsMatch(funName, "^MapType[0-9]*Store$")) {
+										funName = string.Format("[{0}:=]", arity);
 
-										if (!storeFunctions.TryGetValue (arity, out fn)) {
-											fn = currModel.MkFunc (funName, arity);
-											storeFunctions.Add (arity, fn);
+										if (!storeFunctions.TryGetValue(arity, out fn)) {
+											fn = currModel.MkFunc(funName, arity);
+											storeFunctions.Add(arity, fn);
 										}
 									} else {
-										fn = currModel.MkFunc (funName, arity);
+										fn = currModel.MkFunc(funName, arity);
 									}
 								}
 
 								var args = new Model.Element[fn.Arity];
 
 								for (var idx = 0; idx < fn.Arity; ++idx)
-									args [idx] = GetElt (expr [idx + i - arity - 1]);
+									args[idx] = GetElt(expr[idx + i - arity - 1]);
 
-								fn.AddApp (GetElt (expr [i]), args);
+								fn.AddApp(GetElt(expr[i]), args);
 
 								i++;
 								break;
 							}
 						}
-					} else if (expr.Count == 3 && expr [1] == "->") {
-						var funName = (string)expr [0];
+					} else if (expr.Count == 3 && expr[1] == "->") {
+						var funName = (string)expr[0];
 						Model.Func fn = null;
 
-						fn = currModel.MkFunc (funName, 0);
-						fn.SetConstant (GetElt (lastToken));
+						fn = currModel.MkFunc(funName, 0);
+						fn.SetConstant(GetElt(lastToken));
 					} else
-						BadModel ("unidentified line");
+						BadModel("unidentified line");
 				}
 			}
 		}