From 1f0fdf65fd2d21448427ce6afcdbae556ca54881 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sun, 15 Mar 2015 21:32:07 +0100 Subject: [PATCH] Hopefully a fix for restarts --- solver/mcsolver.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index a60ff332..c4438e76 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -839,14 +839,14 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) begin try search (to_int !n_of_conflicts) (to_int !n_of_learnts); with - | Restart -> () + | Restart -> + 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 - end; - n_of_conflicts := !n_of_conflicts *. env.restart_inc; - n_of_learnts := !n_of_learnts *. env.learntsize_inc; + end done; with | Sat -> ()