More thorough checks for exceeding resource limit (#812)

Sometimes Z3 doesn't tell us that it exceeded its resource limit. So, if
it returns "unknown", with an unknown reason, and the reported resource
count exceeds the provided limit, report that it ran out of resources.

Fixes #803.

Addresses dafny-lang/dafny#4804

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;