test/regress/regress0/eqrange2.smt2


1
2
3
4
5
6
7
8
9
10
11
12

(set-logic AUFBV)
(set-option :arrays-exp true)
(set-info :status unsat)
(declare-sort Element 0)
(declare-const a (Array (_ BitVec 3) Element))
(declare-const b (Array (_ BitVec 3) Element))
(declare-const j (_ BitVec 3))
(assert (eqrange a b (_ bv0 3) j))
(assert (eqrange a b (bvadd j (_ bv1 3))  (_ bv7 3)))
(assert (exists ((i (_ BitVec 3))) (not (= (select a i) (select b i)))))
(check-sat)
(exit)