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 = {