[534] % z3 small.smt2
Failed to verify: a.is_numeral(val, r)
ASSERTION VIOLATION
File: ../src/qe/qe_arith.cpp
Line: 567
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[535] % 
[535] % cat small.smt2
(set-option :model_evaluator.array_equalities false)
(declare-fun a ((Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun b ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun c ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(assert
 (forall ((d Int)
     (i Int)
     (e (Array Int (Array Int Real)))
     (f (Array Int (Array Int Real)))
     (j (Array Int (Array Int Real)))
     (k (Array Int (Array Int Real)))
     (l (Array Int (Array Int Real)))
     (g (Array Int (Array Int Real))))
 (let ((h (c e (b f (b (c (b j (b k (a j))) (b l (b g (a l)))) (a f))))))
  (distinct (select (h d) i) (select (h i) d )))))
(check-sat-using qe_rec)
[536] %