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