Substitution in Z3 java

Question

Noticed that when call substitution in z3, it always simplifies the expression, but in our project, it is necessary to just substitute and keep the original structure. According to the following post, such feature will be fixed, wonder if it is already there? Or if there's any way to turn the simplification off?

substitution in Z3Py

Answer 1

Yes, this problem has been fixed in the unstable branch (see here); this should now behave exactly as expected.