More thorough checks for exceeding resource limit

Source/Provers/SMTLib/ProverInterface.cs

@@ -274,7 +274,7 @@ public virtual void SetAdditionalSmtOptions(IEnumerable<OptionValue> entries)
   {
   }
 
-  public virtual Task<int> GetRCount()
+  public virtual int GetRCount()
   {
     throw new NotImplementedException();
   }

Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs

@@ -174,6 +174,11 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
         if (options.Solver == SolverKind.Z3) {
           var rlimitSExp = responseStack.Pop();
           resourceCount = ParseRCount(rlimitSExp);
+
+          // Sometimes Z3 doesn't tell us that it ran out of resources
+          if (result != Outcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) {
+            result = Outcome.OutOfResource;
+          }
         }
 
         var modelSExp = responseStack.Pop();
@@ -277,9 +282,9 @@ protected override void Send(string s, bool isCommon)
       }
     }
 
-    public override Task<int> GetRCount()
+    public override int GetRCount()
     {
-      return Task.FromResult(resourceCount);
+      return resourceCount;
     }
 
     public override Task<List<string>> UnsatCore()

Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs

@@ -18,6 +18,7 @@ public class SMTLibInteractiveTheoremProver : SMTLibProcessTheoremProver
     private bool processNeedsRestart;
     private ScopedNamer commonNamer;
     private ScopedNamer finalNamer;
+    private int resourceCount;
 
     [NotDelayed]
     public SMTLibInteractiveTheoremProver(SMTLibOptions libOptions, SMTLibSolverOptions options, VCExpressionGenerator gen,
@@ -519,6 +520,14 @@ private async Task<Outcome> CheckSatAndGetResponse(CancellationToken cancellatio
         }
       }
 
+      if (options.Solver == SolverKind.Z3) {
+        resourceCount = ParseRCount(await SendVcRequest($"(get-info :{Z3.RlimitOption})"));
+        // Sometimes Z3 doesn't tell us that it ran out of resources
+        if (result != Outcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) {
+          result = Outcome.OutOfResource;
+        }
+      }
+
       return result;
     }
 
@@ -655,7 +664,7 @@ protected override void PrepareCommon() {
       finalNamer = currentNamer;
     }
 
-    public override async Task<int> GetRCount()
+    public override int GetRCount()
     {
       if (options.Solver != SolverKind.Z3) {
         // Only Z3 currently supports retrieving this value. CVC5
@@ -664,7 +673,7 @@ public override async Task<int> GetRCount()
         return 0;
       }
 
-      return ParseRCount(await SendVcRequest($"(get-info :{Z3.RlimitOption})"));
+      return resourceCount;
     }
 
     /// <summary>

Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs

@@ -1275,6 +1275,9 @@ protected Outcome ParseReasonUnknown(SExpr resp, Outcome initialOutcome)
             currentErrorHandler.OnResourceExceeded("max resource limit");
             result = Outcome.OutOfResource;
             break;
+          case "unknown":
+            result = Outcome.Undetermined;
+            break;
           default:
             result = Outcome.Undetermined;
             HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp);

Source/VCGeneration/Checker.cs

@@ -261,7 +261,7 @@ public TimeSpan ProverRunTime
       get { return proverRunTime; }
     }
 
-    public Task<int> GetProverResourceCount()
+    public int GetProverResourceCount()
     {
       return thmProver.GetRCount();
     }

Source/VCGeneration/Split.cs

@@ -1269,7 +1269,7 @@ public int GetHashCode(List<Block> obj)
         }
       }
 
-      public async Task<(ProverInterface.Outcome outcome, VCResult result, int resourceCount)> ReadOutcome(int iteration, Checker checker, VerifierCallback callback)
+      public (ProverInterface.Outcome outcome, VCResult result, int resourceCount) ReadOutcome(int iteration, Checker checker, VerifierCallback callback)
       {
         Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
         ProverInterface.Outcome outcome = cce.NonNull(checker).ReadOutcome();
@@ -1284,7 +1284,7 @@ public int GetHashCode(List<Block> obj)
             string.Join("\n  ", CoveredElements.Select(s => s.Description).OrderBy(s => s)));
         }
 
-        var resourceCount = await checker.GetProverResourceCount();
+        var resourceCount = checker.GetProverResourceCount();
         var result = new VCResult(
           vcNum: SplitIndex + 1,
           iteration: iteration,

Source/VCGeneration/SplitAndVerifyWorker.cs

@@ -166,7 +166,7 @@ private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Ch
         }
       }
 
-      var (newOutcome, result, newResourceCount) = await split.ReadOutcome(iteration, checker, callback);
+      var (newOutcome, result, newResourceCount) = split.ReadOutcome(iteration, checker, callback);
       lock (this) {
         outcome = MergeOutcomes(outcome, newOutcome);
         totalResourceCount += newResourceCount;