(declare-fun a () Real)  
(declare-fun b () Real) 
(declare-fun c () Real) 
(declare-fun d () Real) 
(declare-fun e () Real)  
(declare-fun f () Real)   
(assert (not (exists ((g Real)) (=>  (xor (and (= (div a (-  g)) 2.0)))   (and (=> (<= 0.0 g b)  (<= (div (* c g) d) e)) (= f 2.0)))))) 
(check-sat)  

ASSERTION VIOLATION
File: ../src/math/lp/int_solver.cpp
Line: 427
lrac.m_r_solver.calc_current_x_is_feasible_include_non_basis() == lrac.m_r_solver.current_x_is_feasible()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB