(set-option :model false)  
(declare-fun a () Real)  
(declare-fun b () Real)  
(declare-fun aa () Real)  
(declare-fun c () Real)  
(declare-fun ab () Real)    
(declare-fun d () Real)  
(declare-fun h () Real)    
(declare-fun e () Real)  
(declare-fun f () Real)  
(declare-fun k () Real)  
(declare-fun l () Real)  
(declare-fun g () Real)  
(declare-fun ad () Real)  
(declare-fun n () Real)  
(declare-fun ae () Real)  
(declare-fun i () Real)  
(declare-fun j () Real)  
(declare-fun o () Real)  
(declare-fun r  () Real)  
(declare-fun ag () Real)  
(declare-fun m () Real)  
(declare-fun p () Real)  
(declare-fun q () Real)  
(declare-fun ai () Real)  
(declare-fun aj () Real)  
(declare-fun ak () Real)  
(declare-fun al () Real)  
(declare-fun an () Real)  
(declare-fun ao  () Real)  
(assert (not (exists ((aq Real)) (=> (and (or (and (= r (div 65 a (div 3 aa aq))) (= o 0.0ae 2.0 ad) (<= 0.0 f (- 4 h )) (<= 0.0 n (- h )  0.0 g)) (< 0.0  ak)) (> 0.0 ag)) (or (= (- d ) m) (=> (<= 0.0 k) (=> (<= 0.0 aq k) (and (<=  o (- ak)) (<= 0.0 (mod (* g aq) (/ 81 b al))) (<= (/ (* g aq) (- b al)) (-  ak)) (<= (+ aq ) ag))) (= (/ 71 c p) 2.0)))))))
(assert (=> (and (xor (and (or (=> (xor (>= 0.0  ab ) (<= 0 an)) (<= 0.0 (+ j) ao))) (= ai q (- n))) (< (- a l) 0)) (= aj 2.0) (< (+ (- 2 e m) ) 0.0 (- c i))) (< 0.0 ao))) 
(assert (= b c (+ i p))) 
(check-sat)

ASSERTION VIOLATION
File: ../src/math/lp/nla_core.cpp
Line: 113
canonize_sign_is_correct(m)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB