More checking

msoos · msoos · commit f9b2f40212c8 · 2025-12-22T21:31:05.000+01:00
diff --git a/src/solver.cpp b/src/solver.cpp
@@ -3757,6 +3757,8 @@ std::vector<std::vector<Lit>> Solver::get_cls_defining_var(uint32_t outer_v) con
     assert(get_clause_query);
     Lit l = varReplacer->get_lit_replaced_with_outer(Lit(outer_v, false));
     Lit l_inter  = map_outer_to_inter(l);
+    assert(l_inter.var() < nVars());
+    assert(value(l_inter) == l_Undef);
     assert(varData[l_inter.var()].removed == Removed::elimed);
     return occsimplifier->get_elimed_clauses_for(outer_v);
 }

Original file line number	Diff line number	Diff line change
`@@ -3757,6 +3757,8 @@ std::vector<std::vector<Lit>> Solver::get_cls_defining_var(uint32_t outer_v) con`
`3757`	`3757`	`assert(get_clause_query);`
`3758`	`3758`	`Lit l = varReplacer->get_lit_replaced_with_outer(Lit(outer_v, false));`
`3759`	`3759`	`Lit l_inter = map_outer_to_inter(l);`
	`3760`	`+ assert(l_inter.var() < nVars());`
	`3761`	`+ assert(value(l_inter) == l_Undef);`
`3760`	`3762`	`assert(varData[l_inter.var()].removed == Removed::elimed);`
`3761`	`3763`	`return occsimplifier->get_elimed_clauses_for(outer_v);`
`3762`	`3764`	`}`