From 8d9e85ff49622bdfa555f2abe457a8b10e75eb7c Mon Sep 17 00:00:00 2001
From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com>
Date: Fri, 15 Dec 2023 22:06:07 -0800
Subject: [PATCH] delete binary clauses that are true at the base level

---
 src/mcsat/bool/bool_plugin.c | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/mcsat/bool/bool_plugin.c b/src/mcsat/bool/bool_plugin.c
index 9e4feefa9..06736418a 100644
--- a/src/mcsat/bool/bool_plugin.c
+++ b/src/mcsat/bool/bool_plugin.c
@@ -866,6 +866,7 @@ void bool_plugin_gc_mark(plugin_t* plugin, gc_info_t* gc_vars) {
 
   bool_plugin_t* bp = (bool_plugin_t*) plugin;
   clause_db_t* db = &bp->clause_db;
+  const mcsat_trail_t* trail = bp->ctx->trail;
 
   uint32_t i;
   float act_threshold;
@@ -910,8 +911,11 @@ void bool_plugin_gc_mark(plugin_t* plugin, gc_info_t* gc_vars) {
       clause_ref = bp->lemmas.data[i];
       assert(clause_db_is_clause(db, clause_ref, true));
       c = clause_db_get_clause(&bp->clause_db, clause_ref);
-      if (c->size <= 2) {
-	gc_info_mark(&bp->gc_clauses, clause_ref);
+      if (c->size == 2) {
+        if (!literal_is_true(c->literals[0], trail) &&
+            !literal_is_true(c->literals[1], trail)) {
+          gc_info_mark(&bp->gc_clauses, clause_ref);
+        }
       }
     }
   }