[808] % z3release small.smt2
sat
[809] % z3release nlsat.shuffle_vars=true rewriter.cache_all=true small.smt2
unsat
[810] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert (forall ((e Real))
  (not (=>
     (= (<= 0 e b) (>= c (* e e)))
     (= c (* (- (+ a 1) d) (- (+ a 1) d)))
     (>= d 0)))))
(check-sat)
[811] %