From 6567d32900f4aa1af8ac1c6db0e6ddd21ed46b55 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 18 Nov 2015 17:37:36 +0100 Subject: [PATCH] Fixed bad decision level updating during pop --- solver/internal.ml | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/solver/internal.ml b/solver/internal.ml index d6dba801..99a89f4a 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -999,14 +999,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S) done; Th.backtrack th_env; (* recover the right tenv *) Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); - if not (Vec.is_empty env.trail_lim) then begin - Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - 1); - Vec.set env.trail_lim 0 env.qhead - end; - if not (Vec.is_empty env.tenv_queue) then begin - Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - 1); - Vec.set env.tenv_queue 0 th_env - end; + Vec.clear env.trail_lim; + Vec.clear env.tenv_queue; assert (Vec.size env.trail_lim = Vec.size env.tenv_queue); assert (env.qhead = Vec.size env.trail); ()