From 573870e0f8cca7ef5ac18da1e8ed1d739cfa6bf7 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Mon, 1 Sep 2014 20:05:28 +0200 Subject: [PATCH] fix #17137 Currently, clones "ts -> ty" are represented as "ts -> ts[=ty]", where the second type symbol is an alias created on the fly for the desired type. The problem comes when we want to clone a theory that contains such a cloning declaration. Since these aliases are "non-citizens" -- they are not properly declared, they are not put in the known_map, and they are not listed as locally declared symbols of the theory -- cloning of the cloning declaration mistakes them for external symbols and ignores them. Thus, the aliased type goes into the cloned theory as is, which provokes the error. The fix consists in an additional test for non-local type symbols. If such a symbol is an alias for a type that is actually cloneable, we conclude that the symbol is not external, but is a mere proxy for the aliased type, and so we clone the type and create a fresh type alias for it. A proper fix would be to always clone type symbols into types and never introduce the proxy type aliases. This is a more intrusive change, however, so let's start with a bandage. --- src/core/theory.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/core/theory.ml b/src/core/theory.ml index ca4ee5968..f8b1cb59f 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 -- GitLab