[564] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_context.h
Line: 277
e_internalized(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
ASSERTION VIOLATION
File: ../src/smt/smt_context.h
Line: 277
e_internalized(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[565] % 
[565] % cat small.smt2
(set-option :rewriter.arith_ineq_lhs true)
(set-option :smt.threads 2)
(declare-fun g ((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 e2 () Real)
(declare-fun a3 () (Array Int (Array Int Real)))
(declare-fun e3 () 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 (g ?a ?n)
(exists ((?i Int) (?j Int)) (xor (xor (<= 203 ?i) (<= ?i ?n) (> 153 ?j) (> ?j ?n)) (distinct (select (?a ?i) ?j) (select (?a ?j) ?i)))))))
(assert (g a0 n))
(assert (distinct a1 (store a0 208 (store (select a0 59) 32 e0))))
(assert (distinct a2 (store a1 99 (store (select a1 174) 166 e1))))
(assert (= a3 (store a2 243 (store (select a2 2) 247 e2))))
(assert (= a4 (store a3 91 (store (select a3 19) 244 e3))))
(assert (= a5 (store a4 43 (store (select a4 220) 135 e4))))
(assert (= a6 (store a5 205 (store (select a5 44) 1 e5))))
(assert (g a6 n))
(check-sat)
[566] %