yuriy0

This should be fixed by d57b349629d29d8b9aeb6e8d23bd275ad7a759e6 (and then subsequent bugs which are revealed by the fixing of this one are fixed in a3a98f519eed9f903728be3e1e4634789d9d3f57 and a0fc283d522d637e3074817f6490c902146d33de). I only ran the Maple...

> it's too bad that the in t63.expected (summing two measures over unit) does not go away Indeed, but that is because of the different nesting of `weight` and `if`;...

> The two outer split of the are the same - doesn't that mean that they could be merged? Yes, but > the simplifier tries (successfully!) not to interchange weights...

> I'm more concerned with the situation where x1/x0 = 0 or x1/x0 > 2. I'm not sure I understand. Did you mean `x1/x0 2` (that is the condition which...

> To elaborate on my "concern": [...] I agree that this is the issue, but I am fairly sure that the issue is caused precisely by the buggy result of...

> Regarding the weights that block things: this is part of the reason why we used to push the weights in as far as possible, to expose the control flow...

t62.0 is unchanged; I don't think I'll be revisiting it for a while. It is somewhat of a tricky edge case, in terms of the solution from SemiAlgebraic being slightly...

I'm not sure what code should be dealing with this. It might help to have a program where such expressions occur and are successfully simplified, as well as the one...

> by residualizing those conditions, i.e., by generating a piecewise(...,...,1) if there are conditions that the kb does not discharge I don't understand what it means for the KB to...

> In that situation, I propose that we still simplify product(piecewise(i=K,f(i),1),i=A..B), but not to f(K) but rather to piecewise(K