Produce error if no unsat core when expecting one

boogie-org · Mar 12, 2024 · 1c95249 · 1c95249
1 parent 64a4b5a
commit 1c95249
Showing 1 changed file with 8 additions and 4 deletions.
diff --git a/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs b/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs
@@ -190,10 +190,14 @@ private async Task<SolverOutcome> CheckSat(CancellationToken cancellationToken)
           errorModel = ParseErrorModel(modelSExp);
         }
 
-        if (options.LibOptions.ProduceUnsatCores && responseStack.Count > 0) {
-          var unsatCoreSExp = responseStack.Pop();
-          if (result == SolverOutcome.Valid) {
-            ReportCoveredElements(unsatCoreSExp);
+        if (options.LibOptions.ProduceUnsatCores) {
+          if (responseStack.Count > 0) {
+            var unsatCoreSExp = responseStack.Pop();
+            if (result == SolverOutcome.Valid) {
+              ReportCoveredElements(unsatCoreSExp);
+            }
+          } else {
+            currentErrorHandler.OnProverError("Solver did not return an unsat core.");
           }
         }