Bug when mixing constraint removal and constraints satisfied by unit propagation
I am triggering buggy behavior in the OPB solver by mixing constraint removal with constraints that get satisfied by unit propagation. In particular, the bug is triggered by the following sequence of operations:
- add constraints (x1 + x2 + x3 <= 2), (x1 + x2 >= 2) and (not(x2) v not(x3))
- check satisfiability: formula is SAT, as expected
- remove (x1 + x2 >= 2)
- add (x2 + x3 >= 2): this should contradict (not(x2) v not(x3)), but no exception is thrown
- check satisfiability: formula should be UNSAT, but SAT is returned instead
I have attached a small Java program that follows this sequence of operations, triggering the bug.