(declare-fun a () (Array (_ BitVec 1) (_ BitVec 1)))
(declare-fun b () (_ BitVec 1))
(assert (distinct (store (store (store a b (select a #b0)) #b0 (select a b)) b (select a b)) a))
(check-sat-using qe2)

ASSERTION VIOLATION
File: ../src/qe/qe_mbp.cpp
Line: 76
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a