diff --git a/src/smt/Model.ml b/src/smt/Model.ml
index 791b26a6..200e7c33 100644
--- a/src/smt/Model.ml
+++ b/src/smt/Model.ml
@@ -155,14 +155,14 @@ let eval (m:t) (t:Term.t) : Value.t option =
       let b = aux b in
       if Value.equal a b then Value.true_ else Value.false_
     | App_cst (c, args) ->
-      try Term.Map.find t m.values
-      with Not_found ->
-        match Cst.view c with
-        | Cst_def udef ->
-          (* use builtin interpretation function *)
-          let args = IArray.map aux args in
-          udef.eval args
-        | Cst_undef _ ->
+      match Cst.view c with
+      | Cst_def udef ->
+        (* use builtin interpretation function *)
+        let args = IArray.map aux args in
+        udef.eval args
+      | Cst_undef _ ->
+        try Term.Map.find t m.values
+        with Not_found ->
           begin match Cst.Map.find c m.funs with
             | fi ->
               let args = IArray.map aux args |> IArray.to_list in
diff --git a/src/th-distinct/Sidekick_th_distinct.ml b/src/th-distinct/Sidekick_th_distinct.ml
index 48690df3..f42dbd0f 100644
--- a/src/th-distinct/Sidekick_th_distinct.ml
+++ b/src/th-distinct/Sidekick_th_distinct.ml
@@ -181,6 +181,8 @@ module Arg = struct
 
   let eval args =
     let module Value = Sidekick_smt.Value in
+    Log.debugf 5
+      (fun k->k "(@[distinct.eval@ %a@])" (Fmt.seq Value.pp) (IArray.to_seq args));
     if
       Iter.diagonal (IArray.to_seq args)
       |> Iter.for_all (fun (x,y) -> not @@ Value.equal x y)