Treat incomplete-arithmetic and model-unavailable (#324)

* Treat incomplete-arithmetic and model-unavailable * Remove error codes from new .expect files * Turn model-unavailable into Undetermined Note, there will be a new Z3 option, `candidate_models`, that Boogie can use to always get a model back. This would be a good option to use, when Boogie and Boogie clients switch to that future version of Z3. See Z3Prover/z3#4924. * Add clarification in comments
boogie-org · Jan 5, 2021 · b03dd2e · b03dd2e
1 parent 0ac2790
commit b03dd2e
Show file tree

Hide file tree

Showing 7 changed files with 3,552 additions and 3 deletions.
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
@@ -76,7 +76,7 @@ condition is for.
 APPEND_LOG_FILE=<bool>    Append, rather than overwrite the log file.
 MEMORY_LIMIT=<int>        Memory limit of the prover in megabytes.
 VERBOSITY=<int>           The higher, the more verbose.
-TIME_LIMIT=<int>          Time limit per verification condition in miliseconds.
+TIME_LIMIT=<int>          Time limit per verification condition in milliseconds.
 
 The generic options may or may not be used by the prover plugin.
 ";

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
@@ -1720,6 +1720,12 @@ public override Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1)
               else
               {
                 labels = CalculatePath(handler.StartingProcId());
+                if (labels.Length == 0)
+                {
+                  // Without a path to an error, we don't know what to report
+                  globalResult = Outcome.Undetermined;
+                  break;
+                }
               }
 
               handler.OnModel(labels, model, result);
@@ -2356,6 +2362,8 @@ private Outcome GetResponse()
             {
               case "incomplete":
               case "(incomplete quantifiers)":
+              case "(incomplete (theory arithmetic))":
+              case "smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))":
                 break;
               case "memout":
                 currentErrorHandler.OnResourceExceeded("memory");

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -163,10 +163,14 @@ public SExpr GetProverResponse()
           if (resp.Arguments.Length == 1 && resp.Arguments[0].IsId)
             if (resp.Arguments[0].Name.Contains("max. resource limit exceeded"))
               return resp;
-            else
+            else {
               HandleError(resp.Arguments[0].Name);
-          else
+              return null;
+            }
+          else {
             HandleError(resp.ToString());
+            return null;
+          }
         }
         else if (resp.Name == "progress")
         {