From ce8920bf8844b0a2ae83a3ebb14c4f4e090a56e1 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 6 Feb 2015 17:16:58 +0100 Subject: [PATCH] Revert "[bugfix] uip clause detection was wrong" This reverts commit 7a5e8e082d2203296574d3a6e9e5d329bd1799c8. --- solver/mcsolver.ml | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 92f9e42d..1c7e6c3a 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -338,23 +338,15 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) let history = ref [c_clause] in clause_bump_activity c_clause; let is_semantic a = match a.var.tag.reason with - | Semantic _ -> true - | _ -> false - in - let is_decision a = match a.var.tag.reason with - | Bcp None -> true - | _ -> false + | Semantic _ -> true + | _ -> false in try while true do let _, 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; match atoms with - | [] -> - L.debug 15 "Found Empty clause"; - is_uip := true; - raise Exit - | [a] when is_decision a -> + | [] | _ :: [] -> L.debug 15 "Found UIP clause"; is_uip := true; raise Exit @@ -364,7 +356,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) | _ -> decr tr_ind; L.debug 20 "Looking at trail element %d" !tr_ind; - assert (!tr_ind >= 0); Either.destruct (Vec.get env.trail !tr_ind) (fun v -> L.debug 15 "%a" St.pp_semantic_var v) (fun a -> match a.var.tag.reason with