From 15bd45abc2323aa38e5764d6ccb8ba9541e0f095 Mon Sep 17 00:00:00 2001
From: Samuel Pilz <samuel.pilz@tuwien.ac.at>
Date: Thu, 9 Jan 2025 05:12:27 +0100
Subject: [PATCH] fix resource limit & timeout handling in CheckSat in
 SMTLibInteractiveTheoremProver

---
 Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
index e58b25eac..3bcff8ba3 100644
--- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
+++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
@@ -252,9 +252,15 @@ public async Task<SolverOutcome> CheckSat(CancellationToken cancellationToken,
             currentErrorHandler.OnModel(labels, model, result);
           }
 
+          // if the solver is out of resources or has timed out, the global result needs to reflect that.
+          if (result == SolverOutcome.OutOfResource || result == SolverOutcome.TimeOut) {
+            globalResult = result;
+          }
+
           Debug.Assert(errorsDiscovered > 0);
           // if errorLimit is 0, loop will break only if there are no more 
-          // counterexamples to be discovered.
+          // counterexamples to be discovered or the solver is out of resources
+          // or has timed out.
           if (labels == null || !labels.Any() || errorsDiscovered == errorLimit)
           {
             break;