(set-option :proof true) 
(declare-fun a () Int) 
(declare-fun b () Int) 
(assert (or (= a 5) (= a 7) (= a 0))) 
(assert (<= (* b b) 0)) 
(check-sat)    

ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 2837
to_app(get_fact(p2))->get_arg(0) == get_fact(p1)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB