From f26f74e119b3dea01dec491fd39222c31b3fac6e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 25 Jan 2019 22:01:17 -0600 Subject: [PATCH] fix: bugfix in construction of slices in SAT/theory interface --- src/core/Internal.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 867fcf3e..b26b7e51 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -1644,8 +1644,8 @@ module Make(Plugin : PLUGIN) invalid_arg "Msat.Internal.slice_propagate" ) - let[@specialise] slice_iter st ~full f : unit = - for i = (if full then 0 else st.th_head) to Vec.size st.trail-1 do + let[@specialise] slice_iter st ~full head f : unit = + for i = (if full then 0 else head) to Vec.size st.trail-1 do let e = match Vec.get st.trail i with | Atom a -> Solver_intf.Lit a.lit @@ -1658,7 +1658,7 @@ module Make(Plugin : PLUGIN) let[@inline] current_slice st : (_,_,_) Solver_intf.slice = { Solver_intf. - iter_assumptions=slice_iter st ~full:false; + iter_assumptions=slice_iter st ~full:false st.th_head; push = slice_push st; propagate = slice_propagate st; raise_conflict=slice_raise st; @@ -1667,7 +1667,7 @@ module Make(Plugin : PLUGIN) (* full slice, for [if_sat] final check *) let[@inline] full_slice st : (_,_,_) Solver_intf.slice = { Solver_intf. - iter_assumptions=slice_iter st ~full:true; + iter_assumptions=slice_iter st ~full:true st.th_head; push = slice_push st; propagate = slice_propagate st; raise_conflict=slice_raise st;