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

Extremely verbose message added (to be removed later)

Browse source
This commit is contained in:
Guillaume Bury 2015-03-15 21:55:29 +01:00
parent 34141f9d7d
commit c5fd429821
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
solver/mcsolver.ml
View file

@ -627,8 +627,11 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
add_clause (fresh_tname ()) atoms (Lemma lemma) add_clause (fresh_tname ()) atoms (Lemma lemma)
let slice_propagate f lvl = let slice_propagate f lvl =
L.debug 100 "entering slice.propagate";
let a = add_atom f in let a = add_atom f in
L.debug 100 "atom added";
Iheap.grow_to_by_double env.order (St.nb_vars ()); Iheap.grow_to_by_double env.order (St.nb_vars ());
L.debug 100 "heap grown";
enqueue_bool a lvl (Semantic lvl) enqueue_bool a lvl (Semantic lvl)
let current_slice () = Th.({ let current_slice () = Th.({