diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml
index 58dc9642..1d5b666b 100644
--- a/src/th-cstor/Sidekick_th_cstor.ml
+++ b/src/th-cstor/Sidekick_th_cstor.ml
@@ -46,6 +46,9 @@ module Make(A : ARG) : S with module A = A = struct
   let on_new_term self _solver n (t:T.t) =
     match A.view_as_cstor t with
     | T_cstor (cstor,args) ->
+      Log.debugf 20
+        (fun k->k "(@[th-cstor.on-new-term@ %a@ :cstor %a@ @[:args@ (@[%a@])@]@]@])"
+            T.pp t Fun.pp cstor (Util.pp_iarray T.pp) args);
       N_tbl.add self.cstors n {n; t; cstor; args};
     | _ -> ()
 
diff --git a/tests/unsat/cstor1.smt2 b/tests/unsat/cstor1.smt2
new file mode 100644
index 00000000..c24e1a6e
--- /dev/null
+++ b/tests/unsat/cstor1.smt2
@@ -0,0 +1,6 @@
+
+(set-info :status unsat)
+(declare-datatypes ((nat 0)) (((succ (pred nat)) (zero))))
+
+(assert (= (succ (succ zero)) (succ zero)))
+(check-sat)