1 2 3 4 5 6 7
(set-logic ALL) (set-option :finite-model-find true) (set-info :status sat) (declare-fun v () Bool) (declare-fun v2 () Bool) (assert (exists ((q (Array Bool (Array Bool (Array Int Bool))))) (forall ((q3 (Array Bool (Array Bool (Array Int Bool))))) (xor v2 v2 v v2 (or v2 (not (= q3 q))))))) (check-sat)