From 623893309558450f7ecca692ef0bb6af69df9e3d Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Thu, 28 Jan 2010 00:56:27 +0000
Subject: Fixed bug in DEFTYPE declarations for maps.  Made sure that argument
 and result types of maps are declared before the type of the map itself.

---
 Source/Provers/Z3/TypeDeclCollector.ssc | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Source/Provers/Z3/TypeDeclCollector.ssc b/Source/Provers/Z3/TypeDeclCollector.ssc
index 80d4c4a5..21aebabe 100644
--- a/Source/Provers/Z3/TypeDeclCollector.ssc
+++ b/Source/Provers/Z3/TypeDeclCollector.ssc
@@ -98,18 +98,20 @@ namespace Microsoft.Boogie.Z3
       if (KnownTypes.ContainsKey(type)) return;
       
       if (type.IsMap && CommandLineOptions.Clo.UseArrayTheory) {
+        KnownTypes.Add(type, true);
         string declString = "";
         MapType! mapType = type.AsMap;
         
         declString += "(DEFTYPE " +  TypeToString(type) + " :BUILTIN Array ";
 		foreach (Type! t in mapType.Arguments) {
+		  RegisterType(t);
 		  declString += TypeToString(t);
 		  declString += " ";
 		}
+		RegisterType(mapType.Result);
 		declString += TypeToString(mapType.Result);
 		declString += ")";
-		AddDeclaration(declString);
-		KnownTypes.Add(type, true);
+		AddDeclaration(declString);		
 		return;
       }
       
-- 
cgit v1.2.3