diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 638ffdc0..02c759ca 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -674,7 +674,12 @@ module Make(A : ARG) List.iter (fun f->f()) on_exit; in self.si.on_progress <- (fun () -> on_progress self); - let r = Sat_solver.solve ~assumptions (solver self) in + let on_conflict = + if Profile.enabled() + then Some (fun _ -> Profile.instant "sat.conflict") + else None + in + let r = Sat_solver.solve ?on_conflict ~assumptions (solver self) in Stat.incr self.count_solve; match r with | Sat_solver.Sat st ->