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.

1 files changed, 0 insertions, 2 deletions

diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index f86328d5d..d03b0795f 100644
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -69,8 +69,6 @@ class ArithIteUtils {
   typedef std::map<Node, std::set<Node> > ImpMap;
   ImpMap d_implies;
 
-  std::vector<Node> d_skolemsAdded;
-
   std::vector<Node> d_orBinEqs;
 
 public: