From 5b0a2ad4a4cdcf135f7ff93188d2d624509a45b8 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 15 Feb 2022 16:57:25 -0500
Subject: [PATCH] debug

---
 src/smt-solver/Sidekick_smt_solver.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml
index 8e17923d..6432307a 100644
--- a/src/smt-solver/Sidekick_smt_solver.ml
+++ b/src/smt-solver/Sidekick_smt_solver.ml
@@ -853,6 +853,7 @@ module Make(A : ARG)
       f self.si
         ~add:(fun t u ->
           if not (M.mem model t) then (
+            Log.debugf 20 (fun k->k "(@[smt.model-complete@ %a@ :with-val %a@])" Term.pp t Term.pp u);
             M.replace model t u
           ));
     in
@@ -869,7 +870,10 @@ module Make(A : ARG)
 
         (* try each model hook *)
         let rec try_hooks_ = function
-          | [] -> N.term repr
+          | [] ->
+            let t = N.term repr in
+            Log.debugf 20 (fun k->k "(@[smt.model.default-to-repr@ %a@])" Term.pp t);
+            t
           | h :: hooks ->
             begin match h ~recurse:(fun _ n -> val_for_class n) self.si repr with
               | None -> try_hooks_ hooks