(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert
 (or
  (forall ((e Real))
   (and (or (>= (/ a d) 12.0) (>= (+ a d) (+ 5.0 c)) (>= (+ 5.0 c) 0.0))
    (>= (- b) 12.0)))
  (exists ((g Real)) (forall ((f Real)) (exists ((h Real)) true)))))
(check-sat-using (then qe smt))

ASSERTION VIOLATION
File: ../src/qe/qe.cpp
Line: 1764
l_true == m_solver.check()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB