Remove obsolete files.
When we check that t implies u, also check that t /\ u is satisfiable.

This is needed because we sometimes treat size constraints as integer
constraints and sometimes as rational constraints. For example, given
the constraint 2x = 3, we would say it implies the constraint x = 2
because both x <= 1 and x >= 3 are unsatisfiable, and get into a loop.