From 09c898ff0b998438d4f6e5c7dba384e1d04339ee Mon Sep 17 00:00:00 2001
From: elteammate <elteammate@gmail.com>
Date: Tue, 5 Sep 2023 22:05:12 +0300
Subject: [PATCH] Fix assignment with incremental addition of unit clauses with
 eliminated variable

---
 kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt            | 2 ++
 .../src/commonMain/kotlin/org/kosat/ReconstructionStack.kt    | 4 +++-
 2 files changed, 5 insertions(+), 1 deletion(-)

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
+                }
             }
         }