GitLab

Hello,

For the support of counterexamples, I am trying to add meta on a polymorphic functions but it seems that the transformation encoding_smt_if_poly breaks the meta I introduced when it monomorphizes the function. I would have expected the meta to be adapted (by the transformation) to the generated ident for the monomorphized function.

For example, the following task:

function length (array 'a) : int

(* meta my_meta function length *)

is translated to:

function length ty uni : uni

(* meta my_meta function length1 *)

Note that length1 seem to still refer to the first definition whereas it does not appear anymore in the task: its only apparition is in the meta declaration. Is there a way to keep the meta on my monomorphized function or should I find another solution ?