diff --git a/src/core/theory.ml b/src/core/theory.ml index ca4ee596816bb43f991eecd9b1e16dee10b8b89a..f8b1cb59fbe64336c6a0d2d66c1f5acbbc8fc3e9 100644 --- a/src/core/theory.ml +++ b/src/core/theory.ml @@ -502,7 +502,10 @@ let empty_clones s = { (* populate the clone structure *) let rec cl_find_ts cl ts = - if not (Sid.mem ts.ts_name cl.cl_local) then ts + if not (Sid.mem ts.ts_name cl.cl_local) then + let td = Opt.map (cl_trans_ty cl) ts.ts_def in + if Opt.equal ty_equal ts.ts_def td then ts else + create_tysymbol (id_clone ts.ts_name) ts.ts_args td else try Mts.find ts cl.ts_table with Not_found -> let td' = Opt.map (cl_trans_ty cl) ts.ts_def in