Lines Matching defs:RoundingMode

531     SMTExprRef RoundingMode = getFloatRoundingMode();
534                Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,
539     SMTExprRef RoundingMode = getFloatRoundingMode();
542                Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,
553     SMTExprRef RoundingMode = getFloatRoundingMode();
556                Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,
561     SMTExprRef RoundingMode = getFloatRoundingMode();
564                Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,
698     SMTExprRef RoundingMode = getFloatRoundingMode();
701         Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
706     SMTExprRef RoundingMode = getFloatRoundingMode();
709         Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
714     SMTExprRef RoundingMode = getFloatRoundingMode();
717         Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
722     SMTExprRef RoundingMode = getFloatRoundingMode();
724         Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
729     SMTExprRef RoundingMode = getFloatRoundingMode();
731         Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,