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