Fatal failure at theory/theory_model.cpp:374 (repeat-simp, on-repeat-ite-simp, ite-simp)

[rainoftime]

Related and fixed cvc5/cvc5#3956

---

Hi,
For this formula:

(set-logic NIA)
(set-option :repeat-simp true)
(set-option :on-repeat-ite-simp true)
(set-option :ite-simp true)
(declare-const i0 Int)
(assert (or (= i0 0) (= i0 0)))
(check-sat)

CVC4 (commit. 92ed76819) throws out a fatal failure:

Fatal failure within void CVC4::theory::TheoryModel::addSubstitution(CVC4::TNode, CVC4::TNode, bool) at /home/peisen/test/tofuzz/CVC4/src/theory/theory_model.cpp:374
Internal error detectedTwo incompatible substitutions added to TheoryModel:
the term:    i0
old mapping: (ite deor_1 0 0)
new mapping: (ite deor_2 0 0)
Aborted (core dumped)

[rainoftime]

Another test case

(set-logic QF_ANIA)
(declare-fun _substvar_22_ () (Array Int Bool))
(set-option :ite-simp true)
(set-option :repeat-simp true)
(declare-const i2 Int)
(declare-const arr1 (Array Int Bool))
(declare-const arr2 (Array (Array Int Bool) Int))
(assert (or (= arr2 (store arr2 (store arr1 0 true) i2)) (= arr2 (store arr2 (store arr1 0 true) i2))))
(assert (= arr2 (store arr2 _substvar_22_ i2)))
(check-sat)

[ajreynol]

Could possibly fix this by making ite simplification more deterministic.

[ajreynol]

Second benchmark now gives (error "Arrays cannot be indexed by array types, offending array type is (Array (Array Int Bool) Int)").