Issues on bool-ranged array

[r0ayane]

Hi! For the following instances related to bool-ranged array, the latest yices-smt2 reports unsat while both z3 and cvc5 report sat.

(set-logic QF_ANIA)
(declare-fun v () Bool)
(declare-fun v1 () Bool)
(declare-fun a () (Array Bool Bool))
(assert (select a false))
(assert (or v (select (store a true false) v1)))
(check-sat)

(set-logic QF_ANIA)
(declare-fun v () Bool)
(declare-fun v1 () Bool)
(declare-fun a () (Array Bool Bool))
(assert (select (store (store a false v1) v false) false))
(check-sat)

(set-logic QF_ANIA)
(declare-fun v () Bool)
(declare-fun a () (Array Bool Bool))
(assert (select a true))
(assert (or v (select (store a false false) v)))
(check-sat)

Version:

Yices 2.6.5
Copyright SRI International.
Linked with GMP 6.2.1
Copyright Free Software Foundation, Inc.
Build date: 2024-07-31
Platform: x86_64-pc-linux-gnu (release/static)
Revision: 8e6297e233299631147f98659224c3118fc6a215