test/regress/regress0/aufbv/cee-small-shared-eq.smt2

   1 ; COMMAND-LINE: --ee-mode=distributed
   2 ; COMMAND-LINE: --ee-mode=central
   3 ; EXPECT: sat
   4 (set-logic ALL)
   5 (set-info :status sat)
   6 (declare-fun a () (Array (_ BitVec 1) (_ BitVec 16)))
   7 (assert (not (= (_ bv0 16) (select a ((_ extract 14 14) (select a (_ bv0 1)))))))
   8 (check-sat)