Solve quadratic constraints

[chriseth]

Strategy to solve X * Y = 0:

Go into both branches, figure out that we can solve both for var_8, on the left we have var_8 = L and the right we have var_8 = R. We figure out that L - R is a constant that is at least as large as the range constraint of var_8. This means that L and R cannot both fall into the allowed range for var_8 at the same time. and thus we generate a branch: if L in_range_for var_8 { var_8 = L } else { var_8 = R}

[chriseth]

It seems figuring out L -R is beyond what our current system can do. We would need to add algebraic simplification procedures.

[chriseth]

Oh, maybe it could work using "only known constant is known"-mode