simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 04:05:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Tentative fix for absurd slice size

Browse source
This commit is contained in:
Guillaume Bury 2015-01-24 21:24:03 +01:00
parent f85714537e
commit 8afdc59ced
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
solver/mcsolver.ml
View file

@ -638,7 +638,8 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
}) })
let rec theory_propagate () = let rec theory_propagate () =
let head = Vec.size env.trail in let head = env.qhead in
L.debug 5 "Propagating to theory (with head = %d)" head;
match Th.assume (current_slice ()) with match Th.assume (current_slice ()) with
| Th.Sat -> | Th.Sat ->
L.debug 5 "env.tatoms_qhead : %d -> %d" env.tatoms_qhead head; L.debug 5 "env.tatoms_qhead : %d -> %d" env.tatoms_qhead head;