La_generic Rule Misses Cases
The way La_generic is described it cannot be used on these three linear inequalities:
(1 * x3 + 5 < 1 * x4 + 7)
(not ((8 * x1 - 8 * x2 - 8) = (5 * x3 - 5 * x4 - 10)))
(not (1 * x1 + 3 < 1 * x2 + 4))This should not be the case and Carcara already accepts linear inequalities like this one by flipping the inequality:
(1 * x1 + 3 < 1 * x2 + 4) to ( 1 * x2 + 4 >= 1 * x1 + 3)
Now the terms can be summed up as described in the last step of the la_generic algorithm.