This patch fixes two bugs:
- test1: Previously assume(a >= 5) concluded that a == 5. That's only valid for assume(a == 5)...
- test2: If operands were swapped, additional users were added to the wrong cmp operand. This resulted in an "unsettled iteration" assertion failure.