Pierre Villemot
Pierre Villemot
Of course, I tried to fix this bug by modifying `Uf.assign_next` and `X.assign_value` but it is not sufficient. I will investigate later.
I think we have to accept `Name { ns = User; _ }` in `is_model_term` too?
Basically, that was my patch but I changed `Expr.compare` instead of changing the depth of formula. I still got issues with arrays but I did not search further because it...
Uhm I see. I thought it was okay to use a User defined term as a value.
Do you know how to fix this issue. I quickly took a look to our codebase and Dolmen and we have no mechanism to disable Typer extension like `bv2nat`. We...
Sure, I think about it because I am writing documentation.
Kill it with fire.
@bclement-ocp did you address this issue in your PR for FPA support?
Thanks for reporting this issue. It seems there are at least two issues here (and maybe three?): 1. We don't increment steps in the reasoner of the `Arrays` theory. 2....
I believe we already implement the `extensionality witness technique`: ```ocaml (* nouvelles disegalites par instantiation du premier axiome d'exentionnalite *) let extensionality accu la _class_of = List.fold_left (fun ((env, acc)...