From 3168d4ae2bdf6fce3fa77f8876a31999268c2258 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 8 Dec 2015 13:11:05 +0100 Subject: [PATCH] Fixed bug in if_sat The trick using a bool ref to see if a new clause has been pushed did not detect cases where new clauses were added using assume. --- solver/internal.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/solver/internal.ml b/solver/internal.ml index 6c0f58de..922b24ae 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -682,11 +682,11 @@ module Make propagate = slice_propagate; }) - let full_slice tag = Th.({ + let full_slice () = Th.({ start = 0; length = Vec.size env.elt_queue; get = slice_get; - push = (fun cl proof -> tag := true; slice_push cl proof); + push = slice_push; propagate = (fun _ -> assert false); }) @@ -887,9 +887,11 @@ module Make n_of_conflicts := !n_of_conflicts *. env.restart_inc; n_of_learnts := !n_of_learnts *. env.learntsize_inc | Sat -> - let tag = ref false in - Th.if_sat (full_slice tag); - if not !tag then raise Sat + let nbc = env.nb_init_clauses in + Th.if_sat (full_slice ()); + if env.nb_init_clauses = nbc && + env.elt_head = Vec.size env.elt_queue then + raise Sat end done with