% z3-9be7bda bug.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_internalizer.cpp
Line: 357
!gate_ctx
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
ASSERTION VIOLATION
File: ../src/ast/ast.h
Line: 932
is_app(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
% cat bug.smt2
(set-option :smt.arith.eager_eq_axioms false) 
(set-option :trace true) 
(set-option :smt.arith.propagate_eqs false) 
(declare-fun n () Int) 
(declare-fun x () Int) 
(assert (> n 4)) 
(assert (>= (div 95 x n) n)) 
(check-sat)