519     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPMul()  local
522                Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPMul()
527     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPDiv()  local
530                Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPDiv()
541     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPAdd()  local
544                Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPAdd()
549     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPSub()  local
552                Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPSub()
686     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPtoFP()  local
689         Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPtoFP()
694     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkSBVtoFP()  local
697         Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkSBVtoFP()
702     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkUBVtoFP()  local
705         Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkUBVtoFP()
710     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPtoSBV()  local
712         Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPtoSBV()
717     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPtoUBV()  local
719         Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPtoUBV()