1 2 3 4 5 6 7 8 9 10
; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: unsat (set-logic QF_FP) (set-info :status unsat) (declare-fun x () (_ FloatingPoint 3 5)) (assert (fp.isNegative (fp.abs (fp.neg x)))) (check-sat)