Interaction of smt encoding with meta
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 ?