From f4066b5be3b5473f5c64ab71d1983df6ca7aec76 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 3 Dec 2010 09:26:08 -0800 Subject: Initial implementation of AnalyseFinal --- src/sat/bsat/satSolver.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/sat/bsat/satSolver.c') diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 10dea1e3..1f02adec 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -976,7 +976,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT #endif s->stats.conflicts++; conflictC++; if (sat_solver_dlevel(s) == s->root_level){ -// lit p = clause_is_lit(confl)? clause_read_lit(confl) : clause_begin(confl)[0]; + lit p = clause_is_lit(confl)? clause_read_lit(confl) : clause_begin(confl)[0]; // sat_solver_analyze_final(s, lit_neg(p), &s->conf_final); veci_delete(&learnt_clause); return l_False; -- cgit v1.2.3