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;