Yes, this problem has been fixed in the unstable branch (see here); this should now behave exactly as expected.
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?
Solution
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow