Merge pull request #189 from michael-emmi/z3-params

Using old Z3 model_compress parameter for Dafny.
boogie-org · Jan 20, 2020 · fa23b70 · fa23b70
2 parents 044e533 + 3afaa7d
commit fa23b70
Showing 1 changed file with 26 additions and 13 deletions.
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
@@ -154,9 +154,10 @@ static void FindExecutable()
 
         static int Z3MajorVersion = 0;
         static int Z3MinorVersion = 0;
+        static int Z3PatchVersion = 0;
         static bool Z3VersionObtained = false;
 
-        public static void GetVersion(out int major, out int minor)
+        public static void GetVersion(out int major, out int minor, out int patch)
         {
             if (!Z3VersionObtained)
             {
@@ -181,10 +182,16 @@ public static void GetVersion(out int major, out int minor)
                             var spacebeforefirstdot = answer.LastIndexOf(' ', firstdot);
                             if (spacebeforefirstdot >= 0)
                             {
-                                var majorstr = answer.Substring(spacebeforefirstdot, firstdot - spacebeforefirstdot);
-                                var minorstr = answer.Substring(firstdot + 1, seconddot - firstdot - 1);
-                                Z3MajorVersion = Convert.ToInt32(majorstr);
-                                Z3MinorVersion = Convert.ToInt32(minorstr);
+                                var spaceafterseconddot = answer.IndexOf(' ', seconddot + 1);
+                                if (spaceafterseconddot >= 0) {
+
+                                    var majorstr = answer.Substring(spacebeforefirstdot, firstdot - spacebeforefirstdot);
+                                    var minorstr = answer.Substring(firstdot + 1, seconddot - firstdot - 1);
+                                    var patchstr = answer.Substring(seconddot + 1, spaceafterseconddot - seconddot - 1);
+                                    Z3MajorVersion = Convert.ToInt32(majorstr);
+                                    Z3MinorVersion = Convert.ToInt32(minorstr);
+                                    Z3PatchVersion = Convert.ToInt32(patchstr);
+                                }
                             }
                         }
                     }
@@ -193,12 +200,13 @@ public static void GetVersion(out int major, out int minor)
             }
             major = Z3MajorVersion;
             minor = Z3MinorVersion;
+            patch = Z3PatchVersion;
         }
 
         public static string SetTimeoutOption()
         {
-            int major, minor;
-            GetVersion(out major, out minor);
+            int major, minor, patch;
+            GetVersion(out major, out minor, out patch);
             if (major > 4 || major == 4 && minor >= 3)
                 return "TIMEOUT";
             else
@@ -207,8 +215,8 @@ public static string SetTimeoutOption()
 
         public static string SetRlimitOption()
         {
-            int major, minor;
-            GetVersion(out major, out minor);
+            int major, minor, patch;
+            GetVersion(out major, out minor, out patch);
             if (major > 4 || major == 4 && minor >= 3)
                 return "RLIMIT";
             else
@@ -224,8 +232,8 @@ public static void SetupOptions(SMTLibProverOptions options)
         // throws ProverException, System.IO.FileNotFoundException;
         {
           FindExecutable();
-          int major, minor;
-          GetVersion(out major, out minor);
+          int major, minor, patch;
+          GetVersion(out major, out minor, out patch);
           if (major > 4 || major == 4 && minor >= 3)
           {
 
@@ -289,9 +297,14 @@ public static void SetupOptions(SMTLibProverOptions options)
             options.AddWeakSmtOption("TYPE_CHECK", "true");
             options.AddWeakSmtOption("smt.BV.REFLECT", "true");
 
-            if (major > 4 || (major == 4 && minor >= 8)) {
+            if (major > 4 || (major == 4 && minor >= 8 && patch >= 1)) {
               // {:captureState} does not work with compressed models
-              options.AddWeakSmtOption("model.compact", "false");
+
+              // model_compress was introduced in 4.8.1 and eliminated (consolidated with `model.compact`) in 4.8.7
+              if (patch < 7)
+                  options.AddWeakSmtOption("model_compress", "false");
+              else
+                  options.AddWeakSmtOption("model.compact", "false");
             }
 
             if (options.TimeLimit > 0)