Solution soundness issue on QF_ALIA

[merlinsun]

Hi, for this formula, Z3 5e81c12 gives sat while cvc5 gives unsat.
If r6 is assigned the given model, Z3 returns unsat.

$ z3 delta.smt2
sat
(
  (define-fun r6 () Int
    1)
  (define-fun r () (Array Bool Bool)
    ((as const (Array Bool Bool)) true))
)
$ cat delta.smt2
(declare-fun r () (Array Bool Bool))
(declare-fun r6 () Int)
(assert (and (select r true) (not (select r (= (abs r6) (abs (abs r6)))))))
(check-sat)
(get-model)
$ z3 d.smt2
unsat
$ cat d.smt2
(declare-fun r () (Array Bool Bool))
(declare-fun r6 () Int)
(assert (and (select r true) (not (select r (= (abs 1) (abs (abs 1)))))))
(check-sat)