(set-option :proof true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(assert (forall ((f Real)) (and (or (and (> d (/ 0 b)) (= c 0)) (<= e 0)) (= d a))))
(check-sat)

[561] % z3-4.8.7 small.smt2
unknown
[562] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 2904
to_app(get_fact(p1))->get_decl() == to_app(get_fact(p2))->get_decl() || ( (is_eq(get_fact(p1)) || is_oeq(get_fact(p1))) && (is_eq(get_fact(p2)) || is_oeq(get_fact(p2))))
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[563] % 
[563] % cat small.smt2
(set-option :proof true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(assert (forall ((f Real)) (and (or (and (> d (/ 0 b)) (= c 0)) (<= e 0)) (= d a))))
(check-sat)