If you run our solver on examples/simple_bounds_test.smt2, you will see that it chooses to split a variable over and over and over until we reach maxNumberOfSplits. It does that because the gain is too small, even though the contraction of x from (-inf, 2) to (-inf, -2) would be possible.
I think this has to do with the fact that we use a bigM notation, and that a diameter improvement of 4 is negligable to bigM, so the gain is too small.
However, in the example file (simple_bounds_test), exactly that improvement would result in UNSAT, but we can't detect it.
@kperun
What should we do in this case? Should we just leave it like that?
If you run our solver on examples/simple_bounds_test.smt2, you will see that it chooses to split a variable over and over and over until we reach maxNumberOfSplits. It does that because the gain is too small, even though the contraction of x from (-inf, 2) to (-inf, -2) would be possible.
I think this has to do with the fact that we use a bigM notation, and that a diameter improvement of 4 is negligable to bigM, so the gain is too small. However, in the example file (simple_bounds_test), exactly that improvement would result in UNSAT, but we can't detect it.
@kperun What should we do in this case? Should we just leave it like that?