Mcsat -- keep binary clauses (#436)

* keep binary clauses * disabled problematic regression test * fix
SRI-CSL · Mar 28, 2023 · db89858 · db89858
1 parent eb46358
commit db89858
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 0 deletions.
diff --git a/src/mcsat/bool/bool_plugin.c b/src/mcsat/bool/bool_plugin.c
@@ -863,6 +863,7 @@ void bool_plugin_gc_mark(plugin_t* plugin, gc_info_t* gc_vars) {
   uint32_t i;
   variable_t var;
   clause_ref_t clause_ref;
+  mcsat_clause_t* c;
 
   if (gc_vars->level == 0) {
 
@@ -885,6 +886,16 @@ void bool_plugin_gc_mark(plugin_t* plugin, gc_info_t* gc_vars) {
       clause_ref = bool_plugin_get_reason_ref(bp, var);
       gc_info_mark(&bp->gc_clauses, clause_ref);
     }
+
+    // keep binary clauses
+    for (i = 0; i < bp->lemmas.size; ++ i) {
+      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);
+      }
+    }
   }
 
   // Mark all the CNF definitions

diff --git a/..._brp_withassume.t2__terminationS_7_0.smt2 → ...assume.t2__terminationS_7_0.smt2.disabled b/..._brp_withassume.t2__terminationS_7_0.smt2 → ...assume.t2__terminationS_7_0.smt2.disabled