output "plus:{stringify:{{a}} times:{minus:{stringify:{{b}} stringify:{{d}}} stringify:{{c}}}}";
output "times:{minus:{plus:{stringify:{{a}} stringify:{{b}}} stringify:{{d}}} stringify:{{c}}}";
output "minus:{plus:{stringify:{{a}} stringify:{{b}}} times:{stringify:{{d}} stringify:{{c}}}}";
output "plus:{stringify:{{a}} times:{minus:{stringify:{{b}} stringify:{{d}}} stringify:{{c}}}}";
output "times:{minus:{plus:{stringify:{{a}} stringify:{{b}}} stringify:{{d}}} stringify:{{c}}}";
output "minus:{plus:{stringify:{{a}} stringify:{{b}}} times:{stringify:{{d}} stringify:{{c}}}}";
- output "smt:{while:{>:{{x} {0}} while:{>:{{y} {0}} sbb:{{f o o} {b a r}}}}}";
- output "smt:{while:{>:{{x} {0}} sbb:{while:{>:{{y} {0}} {f o o}} {b a r}}}}";
+ output "smt:{while:{>:{{x} {0}} sbb:{while:{>:{{y} {0}} {f o o}} {b a r}}} while:{>:{{x} {0}} while:{>:{{y} {0}} sbb:{{f o o} {b a r}}}}}";
+ output "smt:{while:{>:{{x} {0}} sbb:{while:{>:{{y} {0}} {f o o}} {b a r}}} while:{>:{{x} {0}} sbb:{while:{>:{{y} {0}} {f o o}} {b a r}}}}";