[506] % z3release small.smt2
unsat
sat
[507] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun g () Real)
(assert
 (not
 (exists ((e Real))
  (forall ((f Real))
  (=> (xor (=> (= f 0) (= a 0))
     (>= (+ (* (/ (- 1) b) e e) g) d)
     (<= (/ (- 1) b e a) c))
   (> b 0)
   (>= (div (to_int a) (to_int a)) (- b)))))))
(check-sat)
(reset)
(define-fun a () Real 0.0)
(define-fun b () Real 1.0)
(define-fun c () Real (- 2.0))
(define-fun d () Real 1.0)
(define-fun g () Real 0.0)
(assert
 (not
 (exists ((e Real))
  (forall ((f Real))
  (=> (xor (=> (= f 0) (= a 0))
     (>= (+ (* (/ (- 1) b) e e) g) d)
     (<= (/ (- 1) b e a) c))
   (> b 0)
   (>= (div (to_int a) (to_int a)) (- b)))))))
(check-sat)
[508] %