From 9c8e970b8dc81ee19f20dae2d3dba9f0f57d9bb2 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 9 Feb 2015 17:10:45 +0100 Subject: [PATCH] [bugfix] level 0 conflict in mcsat weren't detected --- solver/mcsolver.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 3818b0d7..5ac33168 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -327,7 +327,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) let backtrack_lvl is_uip = function | [] -> 0 - | a :: r when not is_uip -> a.var.level - 1 + | a :: r when not is_uip -> max (a.var.level - 1) 0 | a :: [] -> 0 | a :: b :: r -> assert(a.var.level <> b.var.level); b.var.level @@ -342,9 +342,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) | _ -> false in try while true do - let _, atoms = max_lvl_atoms !c in + let lvl, atoms = max_lvl_atoms !c in L.debug 15 "Current conflict clause :"; List.iter (fun a -> L.debug 15 " |- %a" St.pp_atom a) !c; + if lvl = 0 then raise Exit; match atoms with | [] | _ :: [] -> L.debug 15 "Found UIP clause";