1 2 3 4 5 6 7 8 9 10 11
; COMMAND-LINE: -q ; EXPECT: sat ; REQUIRES: symfpu (set-logic HO_ALL) (set-option :assign-function-values false) (set-info :status sat) (declare-fun b () (_ BitVec 1)) (declare-fun c () (_ BitVec 8)) (declare-fun d () (_ BitVec 23)) (assert (= 0 (fp.to_real (fp b c d)))) (check-sat)