Fix infinite loop in arith_ite_simp (#4805)
We have an open issue with an infinite loop with --ite-simp for a long time in #789 , for example on
(declare-fun a () Int)
(declare-fun b () Int)
(assert
(and
(= 1 (+ a b))
(or (= 0 a) (= 0 b))
(or (= 0 b) (>= b 8))
(or (= 0 a) (not (>= b 8)))
)
)
(check-sat)
The problem goes back to arith_ite_utils.cpp and roughly is as follows:
The method solveBinOr looks for patterns like (or (= b 0) (= b 1)). It introduces a new Boolean variable deor_1 and substitutes b -> (ite deor_1 1 0).
The method also stores another mapping in d_skolems: deor_1 -> (>= b 8) here which is also used in selectForCmp. However, these skolems are also used to add even more substitutions here after applying the already added substitutions to it. Eventually, we have a substitution deor_1 -> (>= (ite deor_1 1 0) 8) which inevitably leads to an infinite loop.
I have found no reason for the second mapping (deor_1 -> (>= b 8)) to be added as a substitution, and thus this PR removes it.
Benchmarks are running to check whether there are further issues with this, and whether this simplification is beneficial.
Fixes #789.