(declare-fun symmetric (( Array Int ( Array Int Real )) Int) Bool)
(declare-fun n () Int) 
(declare-fun a0 () ( Array Int ( Array Int Real ))) 
(declare-fun e0 () Real) 
(declare-fun a1 () ( Array Int ( Array Int Real ))) 
(declare-fun e1 () Real) 
(declare-fun a2 () ( Array Int ( Array Int Real ))) 
(declare-fun a4 () ( Array Int ( Array Int Real ))) 
(declare-fun e4 () Real) 
(declare-fun a5 () ( Array Int ( Array Int Real )))
(declare-fun e5 () Real) 
(declare-fun a6 () ( Array Int ( Array Int Real ))) 
(assert (forall (( ?a ( Array Int ( Array Int Real ))) (?n Int)) 
(distinct (symmetric ?a n) 
(forall (( ?i Int ) ( ?j Int )) (or (or (>= 1 ?i ) (> ?i ?n ) (<= 1 ?j ) ( <= ?j n )) (= (select (?a ?i) ?j) (select (?a ?j) ?i))))))) 
(assert (symmetric a0 n )) 
(assert (distinct a1 (store a0 0 (store (select a0 0) 0 e0)))) 
(assert (= a2 (store a1 1 (store (select a1 1) 1 e1))))
(assert (= a5 (store a4 4 (store (select a4 4) 4 e4)))) 
(assert (= a6 (store a5 5 (store (select a5 5) 5 e5)))) 
(check-sat-using (then qe-sat))

ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 89
st != BR_DONE || m().get_sort(m_r) == m().get_sort(t)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB