From d95047b65ab3a421c7cb928ed4f23223142a8fb8 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 1 Feb 2019 21:26:32 -0600 Subject: [PATCH] refactor: a debug msg --- src/smt/Congruence_closure.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml index 57946285..49ea41ed 100644 --- a/src/smt/Congruence_closure.ml +++ b/src/smt/Congruence_closure.ml @@ -589,6 +589,8 @@ let pop_levels (self:t) n : unit = Vec.iter (N.set_field N.field_is_pending false) self.pending; Vec.clear self.pending; Vec.clear self.combine; + Log.debugf 15 + (fun k->k "(@[cc.pop-levels %d@ :n-lvls %d@])" n (Backtrack_stack.n_levels self.undo)); Backtrack_stack.pop_levels self.undo n ~f:(fun f -> f()); ()