[537] % for i in $(seq 1 5); do
> timeout -s 9 8 z3debug small.smt2
> done
Killed
ASSERTION VIOLATION
File: ../src/math/lp/nla_core.cpp
Line: 1499
!l_vec.empty() || elists_are_consistent(true)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
Killed
Killed
ASSERTION VIOLATION
File: ../src/math/lp/nla_core.cpp
Line: 1499
!l_vec.empty() || elists_are_consistent(true)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
Killed
ASSERTION VIOLATION
File: ../src/math/lp/nla_core.cpp
Line: 1499
!l_vec.empty() || elists_are_consistent(true)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
Killed
[538] % 
[538] % cat small.smt2
(set-option :smt.phase_selection 1)
(set-option :smt.threads 3)
(declare-fun e (Int) Int)
(define-fun f ((h Int) (a Int) (b Int)) Int (ite (= b 0) a (mod a b)))
(define-fun g ((h Int) (a Int) (b Int)) Int (f h (* a (e b)) h))
(assert (not (forall ((c Int) (d Int) (h Int)) (= (g h 0 c) (g c c d) c))))
(check-sat-using (then simplify purify-arith ctx-solver-simplify))
[539] %