From 227662f7894b08267d436511a0c0e788ccd5da72 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 19 Jul 2021 09:23:32 -0400 Subject: [PATCH] detail --- src/sat/Solver.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index bf729324..33781d60 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -1676,7 +1676,8 @@ module Make(Plugin : PLUGIN) (* Assert that the conflict is indeeed a conflict *) let check_is_conflict_ self (c:Clause.t) : unit = if not @@ Array.for_all (Atom.is_false self.store) c.atoms then ( - invalid_argf "conflict should be false: %a" (Clause.debug self.store) c + Log.debugf 0 (fun k->k"conflict should be false: %a" (Clause.debug self.store) c); + assert false ) (* some boolean literals were decided/propagated within Msat. Now we