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.

1 files 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;

       }