From c5fd429821a583626d5550e0acd143bbed4bda72 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sun, 15 Mar 2015 21:55:29 +0100 Subject: [PATCH] Extremely verbose message added (to be removed later) --- solver/mcsolver.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 794e5e39..17d7dc8a 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -627,8 +627,11 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) add_clause (fresh_tname ()) atoms (Lemma lemma) let slice_propagate f lvl = + L.debug 100 "entering slice.propagate"; let a = add_atom f in + L.debug 100 "atom added"; Iheap.grow_to_by_double env.order (St.nb_vars ()); + L.debug 100 "heap grown"; enqueue_bool a lvl (Semantic lvl) let current_slice () = Th.({