Pierre Villemot
Pierre Villemot
I agree. We can close this issue as the cache is useful for normalization and we didn't notice slow down.
I believe there is no soundness bug here. For instance, for the following input file: ```smt2 (set-logic ALL) (declare-datatype t ((A) (B (i Int)))) (declare-const e t) (assert ((_ is...
Finally, I think that the best solution is to solve this issue by merging #1095 after `v2.6.0`. I add a test #1211 and this issue will be closed after merging...
I think we can remove the milestone on this issue because we do not plan extra works on it before the next release.
As soon as you rebase it, I will do a last pass on this PR but I think it's already good.
Another solution (a bit better in terms of performance I guess) consists in using a different kind of guards to protect the environments during the exploration for optimization. These guards...
I agree we don't need to support incremental asserting after optimization. > Can you expand on that? I don't understand how that would work. After consideration, it seems my idea...
> Are you talking about the example above with `A1`, `A2`, `A3`? It seems to me that this should work. No, I was talking about an idea in my mind....
> Is this really true? Ok, we have to optimize from scratch after each `check-sat`.
Uhm, I see :/