diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt
index 3aba215..abbabd5 100644
--- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt
+++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt
@@ -238,6 +238,8 @@ class CDCL {
         for (assumption in this.assumptions) assignment.freeze(assumption)
         newClauses.clear()
 
+        if (!ok) return finishWithUnsat()
+
         // Check for an immediate level 0 conflict
         propagate()?.let { return finishWithUnsat() }
 
diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/ReconstructionStack.kt b/kosat-core/src/commonMain/kotlin/org/kosat/ReconstructionStack.kt
index 34709bb..0e18dad 100644
--- a/kosat-core/src/commonMain/kotlin/org/kosat/ReconstructionStack.kt
+++ b/kosat-core/src/commonMain/kotlin/org/kosat/ReconstructionStack.kt
@@ -181,7 +181,9 @@ class ReconstructionStack {
             if (clause.size > 1) {
                 solver.attachClause(Clause(clause))
             } else {
-                check(solver.assignment.enqueue(clause[0], null))
+                if (!solver.assignment.enqueue(clause[0], null)) {
+                    solver.ok = false
+                }
             }
         }