From e8e619f3c72ebe465f17d68f5ca76c0fc2f053f8 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 17 Jan 2017 12:29:39 +0100 Subject: [PATCH] Do not decide on unused variables --- src/core/internal.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/core/internal.ml b/src/core/internal.ml index 0db35e98..f8734758 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -369,6 +369,7 @@ module Make let attach_clause c = assert (not c.attached); Log.debugf debug "Attaching %a" (fun k -> k St.pp_clause c); + Array.iter (fun a -> a.var.used <- a.var.used + 1) c.atoms; Vec.push c.atoms.(0).neg.watched c; Vec.push c.atoms.(1).neg.watched c; c.attached <- true; @@ -986,7 +987,10 @@ module Make (* Decide on a new literal, and enqueue it into the trail *) let rec pick_branch_aux atom: unit = let v = atom.var in - if v.v_level >= 0 then begin + if v.used <= 0 then begin + assert (v.used = 0); + pick_branch_lit () + end else if v.v_level >= 0 then begin assert (v.pa.is_true || v.na.is_true); pick_branch_lit () end else match Plugin.eval atom.lit with