From 9e0c79f597f1bd65123219c15383642221a2bc95 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 22 Mar 2021 12:58:05 -0400
Subject: [PATCH] feat: basic model production for th-data

---
 src/th-data/Sidekick_th_data.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml
index 15756f3f..afe359bc 100644
--- a/src/th-data/Sidekick_th_data.ml
+++ b/src/th-data/Sidekick_th_data.ml
@@ -539,8 +539,12 @@ module Make(A : ARG) : S with module A = A = struct
     match ST_cstors.get self.cstors repr with
     | None -> None
     | Some c ->
-      Log.debugf 1 (fun k->k "FIND CSTOR %a" Monoid_cstor.pp c);
-      None
+      Log.debugf 20 (fun k->k "(@[th-data.mk-model.find-cstor@ %a@])" Monoid_cstor.pp c);
+      let args =
+        IArray.map (fun t -> recurse si (SI.cc_add_term si t))
+          c.c_args in
+      let t = A.mk_cstor self.tst c.c_cstor args in
+      Some t
 
   let create_and_setup (solver:SI.t) : t =
     let self = {