Fix issue with ee-mode central with arrays (cvc5#11898)

The array theory requires explicitly being notified about disequalities
between arrays.

When ee-mode=central, we did not configure arrays to request these
notifications.

Fixes cvc5#11889.

Author: ajreynol

src/theory/theory.cpp

@@ -641,7 +641,7 @@ eq::EqualityEngine* Theory::getEqualityEngine()
 
 bool Theory::expUsingCentralEqualityEngine(TheoryId id)
 {
-  return id != THEORY_ARITH;
+  return id != THEORY_ARITH && id != THEORY_ARRAYS;
 }
 
 theory::Assertion Theory::get()

test/regress/cli/CMakeLists.txt

@@ -163,6 +163,7 @@ set(regress_0_tests
   regress0/arrays/issue9043_4.smt2
   regress0/arrays/issue10494.smt2
   regress0/arrays/issue10494-2.smt2
+  regress0/arrays/issue11889-eec-unsat.smt2
   regress0/arrays/proj-issue322-has-term.smt2
   regress0/arrays/proj-issue391-minisat-elim.smt2
   regress0/arrays/proj-issue467-cm.smt2

test/regress/cli/regress0/arrays/issue11889-eec-unsat.smt2

@@ -0,0 +1,10 @@
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: unsat
+(set-logic QF_AUFLIA)
+(declare-fun a () (Array Int Int))
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun g ((Array Int Int)) Int)
+(declare-fun f (Int) Int)
+(assert (and (distinct (f x) (f y)) (= (store a y 0) (store a x 0)) (distinct (g a) (g (store a y 0)))))
+(check-sat)