diff --git a/src/smt/Model.ml b/src/smt/Model.ml
index b3057484..a64d24a1 100644
--- a/src/smt/Model.ml
+++ b/src/smt/Model.ml
@@ -144,7 +144,6 @@ let eval (m:t) (t:Term.t) : Value.t option =
                 | Some v -> v
               end
             | exception Not_found ->
-              Log.debugf 5 (fun k->k "(@[model.eval.undef@ %a@])" Term.pp t);
               raise No_value (* no particular interpretation *)
           end
       end
diff --git a/src/smt/th_bool/Sidekick_th_bool.ml b/src/smt/th_bool/Sidekick_th_bool.ml
index 00666c99..b7d255b7 100644
--- a/src/smt/th_bool/Sidekick_th_bool.ml
+++ b/src/smt/th_bool/Sidekick_th_bool.ml
@@ -13,9 +13,6 @@ type term = Term.t
 (* TODO: Tseitin on the fly when a composite boolean term is asserted.
   --> maybe, cache the clause inside the literal *)
 
-(* TODO: in theory (or terms?) have a way to evaluate custom terms
-   (like formulas) in a given model, for checking models *)
-
 let id_not = ID.make "not"
 let id_and = ID.make "and"
 let id_or = ID.make "or"
@@ -127,7 +124,7 @@ let and_l st l =
   | args -> Term.app_cst st C.and_ (IArray.of_list args)
 
 let or_l st l =
-  match flatten_id id_and l with
+  match flatten_id id_or l with
   | [] -> Term.false_ st
   | l when List.exists Term.is_true l -> Term.true_ st
   | [x] -> x
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 81616e74..170c7904 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -237,6 +237,9 @@ let check_smt_model (solver:Solver.Sat_solver.t) (hyps:_ Vec.t) (m:Model.t) : un
         if (is_true || is_false) && ((b && is_false) || (not b && is_true)) then (
           Error.errorf "(@[check-model.error@ :atom %a@ :model-val %B@ :sat-val %B@])"
             S.Atom.pp a b (if is_true then true else not is_false)
+        ) else (
+          Log.debugf 5
+            (fun k->k "(@[check-model@ :atom %a@ :model-val %B@ :no-sat-val@])" S.Atom.pp a b);
         )
       | Some v ->
         Error.errorf "(@[check-model.error@ :atom %a@ :non-bool-value %a@])"