inox
inox copied to clipboard
ChooseEncoder doesn't transform all the trees
While copying ChooseEncoder
to Stainless, I noticed that it doesn't traverse all the trees (for instance bound expressions in lets), so I've added a transformer to make sure that we traverse everything. We could port this change back to Inox:
https://github.com/epfl-lara/inox/blob/e74baa7fdb9a941f4e4ce8e880b96a32a96c8b59/src/main/scala/inox/solvers/unrolling/ChooseEncoder.scala
https://github.com/epfl-lara/stainless/blob/729aa8b1666f101f82d918f6caeccd18115ec7f8/core/src/main/scala/stainless/extraction/inlining/ChooseEncoder.scala