inox icon indicating copy to clipboard operation
inox copied to clipboard

ChooseEncoder doesn't transform all the trees

Open jad-hamza opened this issue 3 years ago • 0 comments

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

jad-hamza avatar Oct 01 '21 08:10 jad-hamza