1 2 3 4 5 6 7 8 9 10 11
; EXPECT: unsat (set-logic QF_AX) (set-info :status unsat) (declare-fun a () (Array Bool Bool)) (declare-fun b () (Array Bool Bool)) (assert (not (= (select a (= a b)) (select a (not (= a b)))))) (assert (= (select a true) (select a false))) (check-sat)