[512] % for i in $(seq 1 5) ; do timeout -s 9 20 z3 small.smt2; done
Killed
Killed
ASSERTION VIOLATION
File: ../src/smt/smt_model_finder.cpp
Line: 632
t_val != nullptr
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
Killed
Killed
ASSERTION VIOLATION
File: ../src/smt/smt_model_finder.cpp
Line: 632
t_val != nullptr
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
Killed
[513] % 
[513] % cat small.smt2
(set-option :smt.threads 20)
(set-option :smt.phase_selection 5)
(declare-sort m)
(declare-sort n)
(declare-datatypes () ((a f j)))
(declare-datatypes () ((c1 q p t) (c2 (c4 (k c1) (c3 m)))))
(declare-fun o () m)
(declare-fun x () n)
(declare-fun d () a)
(declare-fun u () (Array n a))
(declare-fun h () (Array n c2))
(declare-fun v () (Array n c2))
(declare-fun w () n)
(assert (forall ((e n)) (= (= d f) (= (select u e) (ite (= e w) f j)))))
(assert (forall ((e n)) (=(= (k (select v e)) p) (= (k (select h e)) q))))
(assert
 (=
 (ite (= d f)
  (ite (= (= d j)
     (= (= o (c3 (select v x)))
     (forall ((e n)) (= (k (select h e)) t)))) f j)
  (ite (forall ((e n)) (= (= (k (select h e)) t) (= d f))) f j))
 f))
(check-sat-using (then purify-arith ctx-solver-simplify))
[514] %