From f1fc429b5a3a783198ff532d9662eb392d7504ca Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 19 Nov 2019 19:48:09 -0600
Subject: [PATCH] add basic test for th-cstor

---
 src/th-cstor/Sidekick_th_cstor.ml | 3 +++
 tests/unsat/cstor1.smt2           | 6 ++++++
 2 files changed, 9 insertions(+)
 create mode 100644 tests/unsat/cstor1.smt2

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)