why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2021-03-13T00:53:06+01:00https://gitlab.inria.fr/why3/why3/-/issues/196Interaction of smt encoding with meta2021-03-13T00:53:06+01:00DAILLER SylvainInteraction of smt encoding with metaHello,
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 expe...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 ?Andrei PaskevichAndrei Paskevich