517     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPMul()  local
520                Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPMul()
525     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPDiv()  local
528                Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPDiv()
539     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPAdd()  local
542                Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPAdd()
547     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPSub()  local
550                Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPSub()
684     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPtoFP()  local
687         Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPtoFP()
692     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkSBVtoFP()  local
695         Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkSBVtoFP()
700     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkUBVtoFP()  local
703         Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkUBVtoFP()
708     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPtoSBV()  local
710         Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPtoSBV()
715     SMTExprRef RoundingMode = getFloatRoundingMode();  in mkFPtoUBV()  local
717         Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,  in mkFPtoUBV()