From bb3533599775716a1cd6b58d614090c3b66e2ae3 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 4 Oct 2024 10:46:31 -0700 Subject: [PATCH] cadical: Initialize external propagator prior to adding clauses. (#11264) Co-authored-by: Aina Niemetz --- src/prop/cadical.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index 401b428ed04..8fe0a032da0 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -1013,8 +1013,7 @@ CadicalSolver::CadicalSolver(Env& env, void CadicalSolver::init() { - d_true = newVar(); - d_false = newVar(); + d_solver->set("quiet", 1); // CaDiCaL is verbose by default // walk and lucky phase do not use the external propagator, disable for now if (d_propagator) @@ -1024,9 +1023,11 @@ void CadicalSolver::init() // ilb currently does not play well with user propagators d_solver->set("ilb", 0); d_solver->set("ilbassumptions", 0); + d_solver->connect_external_propagator(d_propagator.get()); } - d_solver->set("quiet", 1); // CaDiCaL is verbose by default + d_true = newVar(); + d_false = newVar(); d_solver->add(toCadicalVar(d_true)); d_solver->add(0); d_solver->add(-toCadicalVar(d_false)); @@ -1238,7 +1239,6 @@ void CadicalSolver::initialize(context::Context* context, d_context = context; d_proxy = theoryProxy; d_propagator.reset(new CadicalPropagator(theoryProxy, context, *d_solver)); - d_solver->connect_external_propagator(d_propagator.get()); if (!d_env.getPlugins().empty()) { d_clause_learner.reset(new ClauseLearner(*theoryProxy, 0));