diff --git a/librz/arch/isa/x86/common.c b/librz/arch/isa/x86/common.c
index b439f3734e..698eeabe2a 100644
--- a/librz/arch/isa/x86/common.c
+++ b/librz/arch/isa/x86/common.c
@@ -1134,9 +1134,9 @@ RZ_IPI RzILOpEffect *init_rmode() {
  */
 #define EXEC_WITH_RMODE(f, ...) \
 	ITE(EQ(VARL("_rmode"), UN(2, 0)), f(RZ_FLOAT_RMODE_RNE, __VA_ARGS__), \
-		(EQ(VARL("_rmode"), UN(2, 1)), f(RZ_FLOAT_RMODE_RTN, __VA_ARGS__), \
-			(EQ(VARL("_rmode"), UN(2, 2)), f(RZ_FLOAT_RMODE_RTP, __VA_ARGS__), \
-				(f(RZ_FLOAT_RMODE_RTZ, __VA_ARGS__)))))
+		ITE(EQ(VARL("_rmode"), UN(2, 1)), f(RZ_FLOAT_RMODE_RTN, __VA_ARGS__), \
+			ITE(EQ(VARL("_rmode"), UN(2, 2)), f(RZ_FLOAT_RMODE_RTP, __VA_ARGS__), \
+				f(RZ_FLOAT_RMODE_RTZ, __VA_ARGS__))))
 
 RzILOpFloat *resize_floating_helper(RzFloatRMode rmode, RzFloatFormat format, RzILOpFloat *val) {
 	return FCONVERT(format, rmode, val);
@@ -1152,13 +1152,14 @@ RzILOpFloat *resize_floating_helper(RzFloatRMode rmode, RzFloatFormat format, Rz
  * \param ctx use_rmode gets set to true
  * \return RzILOpFloat*
  */
-RZ_IPI RzILOpFloat *x86_il_resize_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
-	rz_return_val_if_fail(val && ctx, NULL);
-	ctx->use_rmode = true;
+RZ_IPI ILPureEffectPair x86_il_resize_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
+	ILPureEffectPair ret = { .val = NULL, .eff = NULL };
+	rz_return_val_if_fail(val && ctx, ret);
+
+	ctx->use_rmode = true;
+	ret.eff = SETL("f_val_rm", val);
+	ret.val = EXEC_WITH_RMODE(resize_floating_helper, format, VARL("f_val_rm"));
 
-	/* TODO: Figure out a more elegant solution than to `DUP` the input val. */
-	RzILOpFloat *ret = EXEC_WITH_RMODE(resize_floating_helper, format, DUP(val));
-	rz_il_op_pure_free(val);
 	return ret;
 }
 
@@ -1176,12 +1177,14 @@ RzILOpFloat *sint2f_floating_helper(RzFloatRMode rmode, RzFloatFormat format, Rz
  * \param ctx use_rmode gets set to true
  * \return RzILOpFloat*
  */
-RZ_IPI RzILOpFloat *x86_il_floating_from_int_ctx(RZ_OWN RZ_NONNULL RzILOpBitVector *int_val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
-	rz_return_val_if_fail(int_val && ctx, NULL);
+RZ_IPI ILPureEffectPair x86_il_floating_from_int_ctx(RZ_OWN RZ_NONNULL RzILOpBitVector *int_val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
+	ILPureEffectPair ret = { .val = NULL, .eff = NULL };
+	rz_return_val_if_fail(int_val && ctx, ret);
 
 	ctx->use_rmode = true;
-	RzILOpFloat *ret = EXEC_WITH_RMODE(sint2f_floating_helper, format, DUP(int_val));
-	rz_il_op_pure_free(int_val);
+	ret.eff = SETL("i_val_rm", int_val);
+	ret.val = EXEC_WITH_RMODE(sint2f_floating_helper, format, VARL("i_val_rm"));
+
 	return ret;
 }
 
@@ -1199,11 +1202,14 @@ RzILOpFloat *f2sint_floating_helper(RzFloatRMode rmode, ut32 width, RzILOpFloat
  * \param ctx use_rmode gets set to true
  * \return RzILOpBitVector*
  */
-RZ_IPI RzILOpBitVector *x86_il_int_from_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *float_val, ut32 width, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
-	rz_return_val_if_fail(float_val && ctx, NULL);
+RZ_IPI ILPureEffectPair x86_il_int_from_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *float_val, ut32 width, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
+	ILPureEffectPair ret = { .val = NULL, .eff = NULL };
+	rz_return_val_if_fail(float_val && ctx, ret);
+
 	ctx->use_rmode = true;
-	RzILOpFloat *ret = EXEC_WITH_RMODE(f2sint_floating_helper, width, DUP(float_val));
-	rz_il_op_pure_free(float_val);
+	ret.eff = SETL("f_val_rm", float_val);
+	ret.val = EXEC_WITH_RMODE(f2sint_floating_helper, width, VARL("f_val_rm"));
+
 	return ret;
 }
 
@@ -1216,13 +1222,13 @@ RZ_IPI RzILOpBitVector *x86_il_int_from_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFlo
  * \param ctx use_rmode gets set to true
  * \return RzILOpFloat* sum
  */
-RZ_IPI RzILOpFloat *x86_il_fadd_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
-	rz_return_val_if_fail(x && y && ctx, NULL);
-	ctx->use_rmode = true;
-	RzILOpFloat *ret = EXEC_WITH_RMODE(FADD, DUP(x), DUP(y));
+RZ_IPI ILPureEffectPair x86_il_fadd_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
+	ILPureEffectPair ret = { .val = NULL, .eff = NULL };
+	rz_return_val_if_fail(x && y && ctx, ret);
 
-	rz_il_op_pure_free(x);
-	rz_il_op_pure_free(y);
+	ctx->use_rmode = true;
+	ret.eff = SEQ2(SETL("x_rm", x), SETL("y_rm", y));
+	ret.val = EXEC_WITH_RMODE(FADD, VARL("x_rm"), VARL("y_rm"));
 
 	return ret;
 }
@@ -1236,13 +1242,13 @@ RZ_IPI RzILOpFloat *x86_il_fadd_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x,
  * \param ctx use_rmode gets set to true
  * \return RzILOpFloat* product
  */
-RZ_IPI RzILOpFloat *x86_il_fmul_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
-	rz_return_val_if_fail(x && y && ctx, NULL);
-	ctx->use_rmode = true;
-	RzILOpFloat *ret = EXEC_WITH_RMODE(FMUL, DUP(x), DUP(y));
+RZ_IPI ILPureEffectPair x86_il_fmul_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
+	ILPureEffectPair ret = { .val = NULL, .eff = NULL };
+	rz_return_val_if_fail(x && y && ctx, ret);
 
-	rz_il_op_pure_free(x);
-	rz_il_op_pure_free(y);
+	ctx->use_rmode = true;
+	ret.eff = SEQ2(SETL("x_rm", x), SETL("y_rm", y));
+	ret.val = EXEC_WITH_RMODE(FMUL, VARL("x_rm"), VARL("y_rm"));
 
 	return ret;
 }
@@ -1256,14 +1262,14 @@ RZ_IPI RzILOpFloat *x86_il_fmul_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x,
  * \param ctx use_rmode gets set to true
  * \return RzILOpFloat* difference
  */
-RZ_IPI RzILOpFloat *x86_il_fsub_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
-	rz_return_val_if_fail(x && y && ctx, NULL);
-	ctx->use_rmode = true;
-	// y - x, hence y is the first argument
-	RzILOpFloat *ret = EXEC_WITH_RMODE(FSUB, DUP(y), DUP(x));
+RZ_IPI ILPureEffectPair x86_il_fsub_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
+	ILPureEffectPair ret = { .val = NULL, .eff = NULL };
+	rz_return_val_if_fail(x && y && ctx, ret);
 
-	rz_il_op_pure_free(x);
-	rz_il_op_pure_free(y);
+	ctx->use_rmode = true;
+	ret.eff = SEQ2(SETL("x_rm", x), SETL("y_rm", y));
+	// y - x, hence y is the first argument
+	ret.val = EXEC_WITH_RMODE(FSUB, VARL("y_rm"), VARL("x_rm"));
 
 	return ret;
 }
@@ -1271,8 +1277,9 @@ RZ_IPI RzILOpFloat *x86_il_fsub_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x,
 /**
  * \brief Subtract \p y from \p x (reverse of \ref x86_il_fsub_with_rmode)
  */
-RZ_IPI RzILOpFloat *x86_il_fsubr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
-	rz_return_val_if_fail(x && y && ctx, NULL);
+RZ_IPI ILPureEffectPair x86_il_fsubr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
+	ILPureEffectPair ret = { .val = NULL, .eff = NULL };
+	rz_return_val_if_fail(x && y && ctx, ret);
 	return x86_il_fsub_with_rmode(y, x);
 }
 
@@ -1285,14 +1292,13 @@ RZ_IPI RzILOpFloat *x86_il_fsubr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x
  * \param ctx use_rmode gets set to true
  * \return RzILOpFloat* division
  */
-RZ_IPI RzILOpFloat *x86_il_fdiv_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
-	rz_return_val_if_fail(x && y && ctx, NULL);
-	ctx->use_rmode = true;
-	// y / x, hence y is the first argument
-	RzILOpFloat *ret = EXEC_WITH_RMODE(FDIV, DUP(y), DUP(x));
+RZ_IPI ILPureEffectPair x86_il_fdiv_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
+	ILPureEffectPair ret = { .val = NULL, .eff = NULL };
+	rz_return_val_if_fail(x && y && ctx, ret);
 
-	rz_il_op_pure_free(x);
-	rz_il_op_pure_free(y);
+	ctx->use_rmode = true;
+	ret.eff = SEQ2(SETL("x_rm", x), SETL("y_rm", y));
+	ret.val = EXEC_WITH_RMODE(FDIV, VARL("x_rm"), VARL("y_rm"));
 
 	return ret;
 }
@@ -1300,8 +1306,9 @@ RZ_IPI RzILOpFloat *x86_il_fdiv_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x,
 /**
  * \brief Divide \p y from \p x (reverse of \ref x86_il_fdiv_with_rmode)
  */
-RZ_IPI RzILOpFloat *x86_il_fdivr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
-	rz_return_val_if_fail(x && y && ctx, NULL);
+RZ_IPI ILPureEffectPair x86_il_fdivr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
+	ILPureEffectPair ret = { .val = NULL, .eff = NULL };
+	rz_return_val_if_fail(x && y && ctx, ret);
 	return x86_il_fdiv_with_rmode(y, x);
 }
 
@@ -1313,12 +1320,13 @@ RZ_IPI RzILOpFloat *x86_il_fdivr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x
  * \param ctx  use_rmode gets set to true
  * \return RzILOpFloat* square root
  */
-RZ_IPI RzILOpFloat *x86_il_fsqrt_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
-	rz_return_val_if_fail(x && ctx, NULL);
-	ctx->use_rmode = true;
-	RzILOpFloat *ret = EXEC_WITH_RMODE(FSQRT, DUP(x));
+RZ_IPI ILPureEffectPair x86_il_fsqrt_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_BORROW RZ_NONNULL X86ILContext *ctx) {
+	ILPureEffectPair ret = { .val = NULL, .eff = NULL };
+	rz_return_val_if_fail(x && ctx, ret);
 
-	rz_il_op_pure_free(x);
+	ctx->use_rmode = true;
+	ret.eff = SETL("x_rm", x);
+	ret.val = EXEC_WITH_RMODE(FSQRT, VARL("x_rm"));
 
 	return ret;
 }
@@ -1338,9 +1346,9 @@ RZ_IPI RzILOpEffect *x86_il_set_st_reg_ctx(X86Reg reg, RZ_OWN RZ_NONNULL RzILOpF
 	if (val_format == RZ_FLOAT_IEEE754_BIN_80) {
 		return SETG(x86_registers[reg], F2BV(val));
 	} else {
-		RzILOpFloat *converted_val = x86_il_resize_floating(val, RZ_FLOAT_IEEE754_BIN_80);
+		ILPureEffectPair converted_val = x86_il_resize_floating(val, RZ_FLOAT_IEEE754_BIN_80);
 
-		return SETG(x86_registers[reg], F2BV(converted_val));
+		return SEQ2(converted_val.eff, SETG(x86_registers[reg], F2BV(converted_val.val)));
 	}
 }
 
@@ -1437,6 +1445,14 @@ RZ_IPI RzILOpEffect *x86_il_st_pop() {
 	return SEQ3(set_top, st_shift, set_underflow);
 }
 
+RZ_IPI ILPureEffectPair x86_il_st_pop_with_val() {
+	ILPureEffectPair ret;
+	ret.val = x86_il_get_st_reg(X86_REG_ST0);
+	ret.eff = x86_il_st_pop();
+
+	return ret;
+}
+
 RZ_IPI RzILOpBool *x86_il_get_fpu_flag(X86FPUFlags flag) {
 	RzILOpPure *shifted_fpsw = SHIFTR0(x86_il_get_reg_bits(X86_REG_FPSW, 0, 0), UN(8, flag));
 	return NON_ZERO(UNSIGNED(1, shifted_fpsw));
@@ -1548,8 +1564,24 @@ RZ_IPI RzILOpEffect *x86_il_set_floating_operand_bits_ctx(X86Op op, RZ_OWN RZ_NO
 	case X86_OP_MEM: {
 		ut64 required_format = x86_width_to_format(op.size * BITS_PER_BYTE);
 
-		RzILOpPure *resized_val = required_format == val_format ? val : x86_il_resize_floating(val, required_format);
-		return x86_il_set_mem_bits(op.mem, F2BV(resized_val), bits, pc);
+		RzILOpPure *resized_val;
+		RzILOpEffect *ret = NULL;
+		if (required_format == val_format) {
+			ILPureEffectPair resized = x86_il_resize_floating(val, required_format);
+			resized_val = resized.val;
+			ret = resized.eff;
+		} else {
+			resized_val = val;
+		}
+
+		RzILOpEffect *set_bits = x86_il_set_mem_bits(op.mem, F2BV(resized_val), bits, pc);
+		if (!ret) {
+			ret = set_bits;
+		} else {
+			ret = SEQ2(ret, set_bits);
+		}
+
+		return ret;
 	}
 	case X86_OP_IMM:
 	default:
diff --git a/librz/arch/isa/x86/common.h b/librz/arch/isa/x86/common.h
index 4468ed61e9..55bf58dd99 100644
--- a/librz/arch/isa/x86/common.h
+++ b/librz/arch/isa/x86/common.h
@@ -126,6 +126,11 @@ typedef enum {
 	X86_FPU_C3 = 14,
 } X86FPUFlags;
 
+typedef struct il_pure_effect_pair_t {
+	RzILOpPure *val;
+	RzILOpEffect *eff;
+} ILPureEffectPair;
+
 RZ_IPI bool x86_il_is_st_reg(X86Reg reg);
 
 /* Need to pass in val_size as a param to avoid unnecessary rounding of val. */
@@ -140,15 +145,10 @@ RZ_IPI RzILOpPure *x86_il_get_fpu_stack_top();
 
 RZ_IPI RzILOpEffect *x86_il_st_push_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat val_format, RZ_BORROW X86ILContext *ctx);
 RZ_IPI RzILOpEffect *x86_il_st_pop();
+RZ_IPI ILPureEffectPair x86_il_st_pop_with_val();
 
 #define x86_il_st_push(val, val_format) x86_il_st_push_ctx(val, val_format, ctx)
 
-#define X86_IL_ST_POP(val, eff) \
-	do { \
-		val = x86_il_get_st_reg(X86_REG_ST0); \
-		eff = x86_il_st_pop(); \
-	} while (0)
-
 RZ_IPI RzILOpPure *x86_il_get_fpu_flag(X86FPUFlags flag);
 RZ_IPI RzILOpEffect *x86_il_set_fpu_flag(X86FPUFlags flag, RZ_OWN RZ_NONNULL RzILOpBool *value);
 
@@ -156,17 +156,17 @@ RZ_IPI RzILOpPure *x86_il_fpu_get_rmode();
 
 RZ_IPI RzILOpEffect *init_rmode();
 
-RZ_IPI RzILOpFloat *x86_il_resize_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
-RZ_IPI RzILOpFloat *x86_il_floating_from_int_ctx(RZ_OWN RZ_NONNULL RzILOpBitVector *int_val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
-RZ_IPI RzILOpBitVector *x86_il_int_from_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *float_val, ut32 width, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
+RZ_IPI ILPureEffectPair x86_il_resize_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
+RZ_IPI ILPureEffectPair x86_il_floating_from_int_ctx(RZ_OWN RZ_NONNULL RzILOpBitVector *int_val, RzFloatFormat format, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
+RZ_IPI ILPureEffectPair x86_il_int_from_floating_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *float_val, ut32 width, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
 
-RZ_IPI RzILOpFloat *x86_il_fadd_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
-RZ_IPI RzILOpFloat *x86_il_fmul_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
-RZ_IPI RzILOpFloat *x86_il_fsub_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
-RZ_IPI RzILOpFloat *x86_il_fsubr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
-RZ_IPI RzILOpFloat *x86_il_fdiv_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
-RZ_IPI RzILOpFloat *x86_il_fdivr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
-RZ_IPI RzILOpFloat *x86_il_fsqrt_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
+RZ_IPI ILPureEffectPair x86_il_fadd_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
+RZ_IPI ILPureEffectPair x86_il_fmul_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
+RZ_IPI ILPureEffectPair x86_il_fsub_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
+RZ_IPI ILPureEffectPair x86_il_fsubr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
+RZ_IPI ILPureEffectPair x86_il_fdiv_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
+RZ_IPI ILPureEffectPair x86_il_fdivr_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_OWN RZ_NONNULL RzILOpFloat *y, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
+RZ_IPI ILPureEffectPair x86_il_fsqrt_with_rmode_ctx(RZ_OWN RZ_NONNULL RzILOpFloat *x, RZ_BORROW RZ_NONNULL X86ILContext *ctx);
 
 #define x86_il_resize_floating(val, format)        x86_il_resize_floating_ctx(val, format, ctx)
 #define x86_il_floating_from_int(int_val, format)  x86_il_floating_from_int_ctx(int_val, format, ctx)
diff --git a/librz/arch/isa/x86/il_fp_ops.inc b/librz/arch/isa/x86/il_fp_ops.inc
index ea797e9a3f..2b97f79818 100644
--- a/librz/arch/isa/x86/il_fp_ops.inc
+++ b/librz/arch/isa/x86/il_fp_ops.inc
@@ -94,11 +94,8 @@ IL_LIFTER(fst) {
  * and pops the value off the stack
  */
 IL_LIFTER(fstp) {
-	RzILOpEffect *pop_eff;
-	RzILOpPure *pop_val;
-	X86_IL_ST_POP(pop_val, pop_eff);
-
-	return SEQ2(x86_il_set_floating_op(0, pop_val, RZ_FLOAT_IEEE754_BIN_80), pop_eff);
+	ILPureEffectPair pop = x86_il_st_pop_with_val();
+	return SEQ2(x86_il_set_floating_op(0, pop.val, RZ_FLOAT_IEEE754_BIN_80), pop.eff);
 }
 
 /**
@@ -139,7 +136,7 @@ IL_LIFTER(fldz) {
 #define FPU_LG2 0x3fff9a209a84fbcfULL, 0xf7988f8959ac200dULL
 #define FPU_LN2 0x3ffeb17217f7d1cfULL, 0x79abc9e3b39828efULL
 
-RzILOpFloat *math_const_to_float_ctx(uint64_t upper, uint64_t lower, X86ILContext *ctx) {
+ILPureEffectPair math_const_to_float_ctx(uint64_t upper, uint64_t lower, X86ILContext *ctx) {
 	RzILOpPure *upper_unshifted = UN(128, upper);
 	RzILOpPure *upper_shifted = SHIFTL0(upper_unshifted, UN(8, 8));
 
@@ -158,7 +155,8 @@ RzILOpFloat *math_const_to_float_ctx(uint64_t upper, uint64_t lower, X86ILContex
  * Load log2(10)
  */
 IL_LIFTER(fldl2t) {
-	return x86_il_st_push(math_const_to_float(FPU_L2T), RZ_FLOAT_IEEE754_BIN_80);
+	ILPureEffectPair math_const = math_const_to_float(FPU_L2T);
+	return SEQ2(math_const.eff, x86_il_st_push(math_const.val, RZ_FLOAT_IEEE754_BIN_80));
 }
 
 /**
@@ -166,7 +164,8 @@ IL_LIFTER(fldl2t) {
  * Load log2(e)
  */
 IL_LIFTER(fldl2e) {
-	return x86_il_st_push(math_const_to_float(FPU_L2E), RZ_FLOAT_IEEE754_BIN_80);
+	ILPureEffectPair math_const = math_const_to_float(FPU_L2E);
+	return SEQ2(math_const.eff, x86_il_st_push(math_const.val, RZ_FLOAT_IEEE754_BIN_80));
 }
 
 /**
@@ -174,7 +173,8 @@ IL_LIFTER(fldl2e) {
  * Load pi
  */
 IL_LIFTER(fldpi) {
-	return x86_il_st_push(math_const_to_float(FPU_PI), RZ_FLOAT_IEEE754_BIN_80);
+	ILPureEffectPair math_const = math_const_to_float(FPU_PI);
+	return SEQ2(math_const.eff, x86_il_st_push(math_const.val, RZ_FLOAT_IEEE754_BIN_80));
 }
 
 /**
@@ -182,7 +182,8 @@ IL_LIFTER(fldpi) {
  * Load log10(2)
  */
 IL_LIFTER(fldlg2) {
-	return x86_il_st_push(math_const_to_float(FPU_LG2), RZ_FLOAT_IEEE754_BIN_80);
+	ILPureEffectPair math_const = math_const_to_float(FPU_LG2);
+	return SEQ2(math_const.eff, x86_il_st_push(math_const.val, RZ_FLOAT_IEEE754_BIN_80));
 }
 
 /**
@@ -190,7 +191,8 @@ IL_LIFTER(fldlg2) {
  * Load ln(2)
  */
 IL_LIFTER(fldln2) {
-	return x86_il_st_push(math_const_to_float(FPU_LN2), RZ_FLOAT_IEEE754_BIN_80);
+	ILPureEffectPair math_const = math_const_to_float(FPU_LN2);
+	return SEQ2(math_const.eff, x86_il_st_push(math_const.val, RZ_FLOAT_IEEE754_BIN_80));
 }
 
 /**
@@ -223,9 +225,9 @@ IL_LIFTER(fxch) {
  */
 IL_LIFTER(fild) {
 	RzILOpPure *int_val = x86_il_get_op(0);
-	RzILOpFloat *float_val = x86_il_floating_from_int(int_val, RZ_FLOAT_IEEE754_BIN_80);
+	ILPureEffectPair float_val = x86_il_floating_from_int(int_val, RZ_FLOAT_IEEE754_BIN_80);
 
-	return x86_il_st_push(float_val, RZ_FLOAT_IEEE754_BIN_80);
+	return SEQ2(float_val.eff, x86_il_st_push(float_val.val, RZ_FLOAT_IEEE754_BIN_80));
 }
 
 /**
@@ -233,8 +235,8 @@ IL_LIFTER(fild) {
  * Store float in ST(0) after rounding to integer
  */
 IL_LIFTER(fist) {
-	RzILOpPure *int_val = x86_il_int_from_floating(x86_il_get_st_reg(X86_REG_ST0), ins->structure->operands[0].size * BITS_PER_BYTE);
-	return x86_il_set_op(0, int_val);
+	ILPureEffectPair int_val = x86_il_int_from_floating(x86_il_get_st_reg(X86_REG_ST0), ins->structure->operands[0].size * BITS_PER_BYTE);
+	return SEQ2(int_val.eff, x86_il_set_op(0, int_val.val));
 }
 
 /**
@@ -242,12 +244,9 @@ IL_LIFTER(fist) {
  * Store float in ST(0) after rounding to integer, pop the FPU register stack
  */
 IL_LIFTER(fistp) {
-	RzILOpEffect *pop_eff;
-	RzILOpPure *pop_val;
-	X86_IL_ST_POP(pop_val, pop_eff);
-
-	RzILOpPure *int_val = x86_il_int_from_floating(pop_val, ins->structure->operands[0].size * BITS_PER_BYTE);
-	return SEQ2(x86_il_set_op(0, int_val), pop_eff);
+	ILPureEffectPair pop = x86_il_st_pop_with_val();
+	ILPureEffectPair int_val = x86_il_int_from_floating(pop.val, ins->structure->operands[0].size * BITS_PER_BYTE);
+	return SEQ3(int_val.eff, x86_il_set_op(0, int_val.val), pop.eff);
 }
 
 /**
@@ -279,7 +278,8 @@ IL_LIFTER(fbld) {
 			SETL("i", SUB(VARL("i"), UN(mem_size, 1))) // i--
 			));
 
-	RzILOpEffect *f_init = SETL("f", x86_il_floating_from_int(VARL("val"), RZ_FLOAT_IEEE754_BIN_80));
+	ILPureEffectPair fval = x86_il_floating_from_int(VARL("val"), RZ_FLOAT_IEEE754_BIN_80);
+	RzILOpEffect *f_init = SEQ2(fval.eff, SETL("f", fval.val));
 
 	/* Check sign byte (index 9) checking if sign byte is zero */
 	RzILOpPure *sign_byte = LOADW(8, ADD(VARL("mem"), UN(mem_size, 9)));
@@ -300,11 +300,10 @@ IL_LIFTER(fbld) {
 IL_LIFTER(fbstp) {
 	ut8 mem_size = analysis->bits;
 
-	RzILOpEffect *pop_eff;
-	RzILOpPure *pop_val;
-	X86_IL_ST_POP(pop_val, pop_eff);
+	ILPureEffectPair pop = x86_il_st_pop_with_val();
 
-	RzILOpEffect *val_init = SETL("val", x86_il_int_from_floating(pop_val, 64));
+	ILPureEffectPair val = x86_il_int_from_floating(pop.val, 64);
+	RzILOpEffect *val_init = SEQ2(val.eff, SETL("val", val.val));
 	RzILOpEffect *sgn_init = SETL("sgn", MSB(VARL("val")));
 	RzILOpEffect *val_abs = SETL("val", ITE(VARL("sgn"), NEG(VARL("val")), VARL("val")));
 
@@ -338,7 +337,7 @@ IL_LIFTER(fbstp) {
 		noexcept_case);
 
 	return SEQ5(
-		val_init, pop_eff, // get val from ST(0) and pop
+		val_init, pop.eff, // get val from ST(0) and pop
 		sgn_init, val_abs, // val = |val| and store sign
 		maybe_except);
 }
@@ -358,6 +357,7 @@ IL_LIFTER(fabs) {
 	do { \
 		RzILOpFloat *src; \
 		X86Reg dest_reg; \
+		RzILOpEffect *src_eff = NULL; \
 \
 		/* TODO: Check whether all the enumerated cases here are correct, through \
 		 * code coverage. */ \
@@ -365,7 +365,9 @@ IL_LIFTER(fabs) {
 		case 1: \
 			/* Need to convert a 32-bit or 64-bit memory operand */ \
 			dest_reg = X86_REG_ST0; \
-			src = x86_il_resize_floating(x86_il_get_floating_op(0), RZ_FLOAT_IEEE754_BIN_80); \
+			ILPureEffectPair resized = x86_il_resize_floating(x86_il_get_floating_op(0), RZ_FLOAT_IEEE754_BIN_80); \
+			src = resized.val; \
+			src_eff = resized.eff; \
 			break; \
 		case 2: \
 			/* ST(i) operand, so no need for resizing */ \
@@ -377,8 +379,13 @@ IL_LIFTER(fabs) {
 			return NULL; \
 		} \
 \
-		RzILOpFloat *result = x86_il_##op##_with_rmode(src, x86_il_get_st_reg(dest_reg)); \
-		return x86_il_set_st_reg(dest_reg, result, RZ_FLOAT_IEEE754_BIN_80); \
+		ILPureEffectPair result = x86_il_##op##_with_rmode(src, x86_il_get_st_reg(dest_reg)); \
+		RzILOpEffect *ret = SEQ2(result.eff, x86_il_set_st_reg(dest_reg, result.val, RZ_FLOAT_IEEE754_BIN_80)); \
+\
+		if (src_eff) { \
+			ret = SEQ2(src_eff, ret); \
+		} \
+		return ret; \
 	} while (0)
 
 #define FLOATING_ARITHMETIC_POP_IL(op) \
@@ -390,15 +397,15 @@ IL_LIFTER(fabs) {
 			dest_reg = ins->structure->operands[0].reg; \
 		} \
 \
-		RzILOpPure *result = x86_il_##op##_with_rmode(x86_il_get_st_reg(X86_REG_ST0), x86_il_get_st_reg(dest_reg)); \
-		return SEQ2(x86_il_set_st_reg(dest_reg, result, RZ_FLOAT_IEEE754_BIN_80), x86_il_st_pop()); \
+		ILPureEffectPair result = x86_il_##op##_with_rmode(x86_il_get_st_reg(X86_REG_ST0), x86_il_get_st_reg(dest_reg)); \
+		return SEQ3(result.eff, x86_il_set_st_reg(dest_reg, result.val, RZ_FLOAT_IEEE754_BIN_80), x86_il_st_pop()); \
 	} while (0)
 
 #define FLOATING_INT_ARITHMETIC_IL(op) \
 	do { \
-		RzILOpPure *float_val = x86_il_floating_from_int(x86_il_get_op(0), RZ_FLOAT_IEEE754_BIN_80); \
-		RzILOpPure *result = x86_il_##op##_with_rmode(float_val, x86_il_get_st_reg(X86_REG_ST0)); \
-		return x86_il_set_st_reg(X86_REG_ST0, result, RZ_FLOAT_IEEE754_BIN_80); \
+		ILPureEffectPair float_val = x86_il_floating_from_int(x86_il_get_op(0), RZ_FLOAT_IEEE754_BIN_80); \
+		ILPureEffectPair result = x86_il_##op##_with_rmode(float_val.val, x86_il_get_st_reg(X86_REG_ST0)); \
+		return SEQ3(float_val.eff, result.eff, x86_il_set_st_reg(X86_REG_ST0, result.val, RZ_FLOAT_IEEE754_BIN_80)); \
 	} while (0)
 
 /**
@@ -587,7 +594,8 @@ IL_LIFTER(fcomp) {
  * Compare the floating point value in ST(0) with an integer and store the result in the FPU control word
  */
 IL_LIFTER(ficom) {
-	return fcom_helper(ins, pc, analysis, x86_il_floating_from_int(x86_il_get_op(0), RZ_FLOAT_IEEE754_BIN_80));
+	ILPureEffectPair float_val = x86_il_floating_from_int(x86_il_get_op(0), RZ_FLOAT_IEEE754_BIN_80);
+	return SEQ2(float_val.eff, fcom_helper(ins, pc, analysis, float_val.val));
 }
 
 /**
@@ -604,7 +612,8 @@ IL_LIFTER(fcompp) {
  * Compare the floating point value in ST(0) with an integer, store the result in the FPU control word and pop the stack
  */
 IL_LIFTER(ficomp) {
-	return SEQ2(fcom_helper(ins, pc, analysis, x86_il_floating_from_int(x86_il_get_op(0), RZ_FLOAT_IEEE754_BIN_80)), x86_il_st_pop());
+	ILPureEffectPair float_val = x86_il_floating_from_int(x86_il_get_op(0), RZ_FLOAT_IEEE754_BIN_80);
+	return SEQ2(float_val.eff, SEQ2(fcom_helper(ins, pc, analysis, float_val.val), x86_il_st_pop()));
 }
 
 RzILOpEffect *fcomi_helper(const X86ILIns *ins, ut64 pc, RzAnalysis *analysis) {
@@ -661,10 +670,11 @@ IL_LIFTER(ftst) {
  * Round ST(0) to an integer
  */
 IL_LIFTER(frndint) {
-	return x86_il_set_st_reg(X86_REG_ST0,
-		/* Not very sure about whether the rounded integer should be limited to 64 bits or not. */
-		x86_il_floating_from_int(x86_il_int_from_floating(x86_il_get_st_reg(X86_REG_ST0), 64), RZ_FLOAT_IEEE754_BIN_80),
-		RZ_FLOAT_IEEE754_BIN_80);
+	ILPureEffectPair int_from_float = x86_il_int_from_floating(x86_il_get_st_reg(X86_REG_ST0), 64);
+	ILPureEffectPair float_from_int = x86_il_floating_from_int(int_from_float.val, RZ_FLOAT_IEEE754_BIN_80);
+
+	/* Not very sure about whether the rounded integer should be limited to 64 bits or not. */
+	return SEQ3(int_from_float.eff, float_from_int.eff, x86_il_set_st_reg(X86_REG_ST0, float_from_int.val, RZ_FLOAT_IEEE754_BIN_80));
 }
 
 /**
@@ -672,7 +682,8 @@ IL_LIFTER(frndint) {
  * Calculate the square root of ST(0)
  */
 IL_LIFTER(fsqrt) {
-	return x86_il_set_st_reg(X86_REG_ST0, x86_il_fsqrt_with_rmode(x86_il_get_st_reg(X86_REG_ST0)), RZ_FLOAT_IEEE754_BIN_80);
+	ILPureEffectPair fsqrt_res = x86_il_fsqrt_with_rmode(x86_il_get_st_reg(X86_REG_ST0));
+	return SEQ2(fsqrt_res.eff, x86_il_set_st_reg(X86_REG_ST0, fsqrt_res.val, RZ_FLOAT_IEEE754_BIN_80));
 }
 
 /**
@@ -688,12 +699,8 @@ IL_LIFTER(fnop) {
  * Round ST(0) to an integer (using RZ_FLOAT_RMODE_RTZ), store the integer in the memory operand and pop the stack
  */
 IL_LIFTER(fisttp) {
-	return SEQ2(
-		x86_il_set_op(0,
-			x86_il_int_from_floating(
-				x86_il_get_st_reg(X86_REG_ST0),
-				ins->structure->operands[0].size * BITS_PER_BYTE)),
-		x86_il_st_pop());
+	ILPureEffectPair int_from_float = x86_il_int_from_floating(x86_il_get_st_reg(X86_REG_ST0), ins->structure->operands[0].size * BITS_PER_BYTE);
+	return SEQ3(int_from_float.eff, x86_il_set_op(0, int_from_float.val), x86_il_st_pop());
 }
 
 #include <rz_il/rz_il_opbuilder_end.h>
diff --git a/test/db/asm/x86_64 b/test/db/asm/x86_64
index 12891d1de3..bb59ac290a 100644
--- a/test/db/asm/x86_64
+++ b/test/db/asm/x86_64
@@ -1022,11 +1022,11 @@ ad "xchg rdx, r8" 4c87c2 0x0 (seq (set _temp (var rdx)) (set rdx (var r8)) (set
 ad "xchg r15, rdx" 4987d7 0x0 (seq (set _temp (var r15)) (set r15 (cast 64 false (var rdx))) (set rdx (var _temp)))
 d "call qword [rip + 0x3a8f3e]" 48ff153e8f3a00 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x7))) (set rsp (var final)) (jmp (loadw 0 64 (+ (bv 64 0x7) (bv 64 0x3a8f3e)))))
 d "call qword [rip + 0x1d638f]" 48ff158f631d00 0x0 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x7))) (set rsp (var final)) (jmp (loadw 0 64 (+ (bv 64 0x7) (bv 64 0x1d638f)))))
-a "fmul st2, st0" dcca 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st2 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (float 2 (var st2) ) (float 2 (var st2) )) (*. rtz (float 2 (var st2) ) (float 2 (var st2) ))))))
-a "fdiv st0, st1" d8f1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st1) )) (fconvert ieee754-bin80 rtz (float 2 (var st1) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st1) )) (fconvert ieee754-bin80 rtz (float 2 (var st1) ))))))))
-a "fdiv st(0), st(1)" d8f1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st1) )) (fconvert ieee754-bin80 rtz (float 2 (var st1) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st1) )) (fconvert ieee754-bin80 rtz (float 2 (var st1) ))))))))
-a "fdiv st0, st7" d8f7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))))))))
-a "fdiv st(0), st(7)" d8f7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))))))))
+a "fmul st2, st0" dcca 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st2) )) (set y_rm (float 2 (var st2) )) (set st2 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
+a "fdiv st0, st1" d8f1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st1) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fdiv st(0), st(1)" d8f1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st1) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fdiv st0, st7" d8f7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fdiv st(0), st(7)" d8f7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
 a "fcmove st0, st1" dac9
 a "fcmovbe st0, st1" dad1
 a "fcmovu st0, st1" dad9
@@ -1041,84 +1041,84 @@ a "fxch" d9c9 0x0 (seq (set tmp (float 2 (var st0) )) (set st0 (fbits (float 2 (
 a "fxch st2" d9ca 0x0 (seq (set tmp (float 2 (var st0) )) (set st0 (fbits (float 2 (var st2) ))) (set st2 (fbits (var tmp))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
 ad "fld1" d9e8 0x0 (seq (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (float 2 (bv 80 0x3fff8000000000000000) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
 ad "fldz" d9ee 0x0 (seq (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (float 2 (bv 80 0x0) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-ad "fldl2t" d9e9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x3fffd49a784bcd1b) (bv 8 0x8) false) (bv 128 0x8000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x3fffd49a784bcd1b) (bv 8 0x8) false) (bv 128 0x8000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-ad "fldl2e" d9ea 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x3fffb8aa3b295c17) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x3fffb8aa3b295c17) (bv 8 0x8) false) (bv 128 0xc000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-ad "fldpi" d9eb 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x4000c90fdaa22168) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x4000c90fdaa22168) (bv 8 0x8) false) (bv 128 0xc000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-ad "fldlg2" d9ec 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x3fff9a209a84fbcf) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x3fff9a209a84fbcf) (bv 8 0x8) false) (bv 128 0xc000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-ad "fldln2" d9ed 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 3 (| (<< (bv 128 0x3ffeb17217f7d1cf) (bv 8 0x8) false) (bv 128 0x4000000000000000)) )) (fconvert ieee754-bin80 rtz (float 3 (| (<< (bv 128 0x3ffeb17217f7d1cf) (bv 8 0x8) false) (bv 128 0x4000000000000000)) ))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+ad "fldl2t" d9e9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 3 (| (<< (bv 128 0x3fffd49a784bcd1b) (bv 8 0x8) false) (bv 128 0x8000000000000000)) )) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+ad "fldl2e" d9ea 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 3 (| (<< (bv 128 0x3fffb8aa3b295c17) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+ad "fldpi" d9eb 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 3 (| (<< (bv 128 0x4000c90fdaa22168) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+ad "fldlg2" d9ec 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 3 (| (<< (bv 128 0x3fff9a209a84fbcf) (bv 8 0x8) false) (bv 128 0xc000000000000000)) )) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+ad "fldln2" d9ed 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 3 (| (<< (bv 128 0x3ffeb17217f7d1cf) (bv 8 0x8) false) (bv 128 0x4000000000000000)) )) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
 a "fucom" dde1 0x0 (seq (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) )))) (<. (float 2 (var st0) ) (float 2 (var st1) ))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) ))) (|| (<. (float 2 (var st0) ) (float 2 (var st1) )) (<. (float 2 (var st1) ) (float 2 (var st0) ))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))))
 a "fucom st(2)" dde2 0x0 (seq (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) )))) (<. (float 2 (var st0) ) (float 2 (var st2) ))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) ))) (|| (<. (float 2 (var st0) ) (float 2 (var st2) )) (<. (float 2 (var st2) ) (float 2 (var st0) ))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))))
 a "fucomp" dde9 0x0 (seq (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) )))) (<. (float 2 (var st0) ) (float 2 (var st1) ))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st1) ))) (|| (<. (float 2 (var st0) ) (float 2 (var st1) )) (<. (float 2 (var st1) ) (float 2 (var st0) ))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
 a "fucomp st(2)" ddea 0x0 (seq (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) )))) (<. (float 2 (var st0) ) (float 2 (var st2) ))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (float 2 (var st2) ))) (|| (<. (float 2 (var st0) ) (float 2 (var st2) )) (<. (float 2 (var st2) ) (float 2 (var st0) ))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "faddp" dec1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (float 2 (var st0) ) (float 2 (var st1) )) (+. rtz (float 2 (var st0) ) (float 2 (var st1) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "faddp st2, st0" dec2 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (float 2 (var st0) ) (float 2 (var st1) )) (+. rtz (float 2 (var st0) ) (float 2 (var st1) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fiadd word [rax]" de00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (+. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) ))))))
-a "fiadd dword [rax]" da00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (+. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) ))))))
-a "fadd dword [rax]" d800 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (+. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) ))))))
-a "fadd qword [rax]" dc00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (+. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) ))))))
-a "ficom word [rax]" de10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) ))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))))
-a "ficom dword [rax]" da10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) ))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))))
-a "ficomp word [rax]" de18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) ))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "ficomp dword [rax]" da18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) ))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fild word [rax]" df00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fild dword [rax]" db00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fild qword [rax]" df28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 64 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 64 (+ (var rax) (bv 64 0x0))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "faddp" dec1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (+. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (+. rtp (var x_rm) (var y_rm)) (+. rtz (var x_rm) (var y_rm))))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "faddp st2, st0" dec2 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (+. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (+. rtp (var x_rm) (var y_rm)) (+. rtz (var x_rm) (var y_rm))))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fiadd word [rax]" de00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (+. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (+. rtp (var x_rm) (var y_rm)) (+. rtz (var x_rm) (var y_rm))))))))
+a "fiadd dword [rax]" da00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (+. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (+. rtp (var x_rm) (var y_rm)) (+. rtz (var x_rm) (var y_rm))))))))
+a "fadd dword [rax]" d800 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (+. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (+. rtp (var x_rm) (var y_rm)) (+. rtz (var x_rm) (var y_rm))))))))
+a "fadd qword [rax]" dc00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (+. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (+. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (+. rtp (var x_rm) (var y_rm)) (+. rtz (var x_rm) (var y_rm))))))))
+a "ficom word [rax]" de10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))) (float 2 (var st0) ))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))))
+a "ficom dword [rax]" da10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))) (float 2 (var st0) ))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))))
+a "ficomp word [rax]" de18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))) (float 2 (var st0) ))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "ficomp dword [rax]" da18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set swd (| (<< (ite (&& (! (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))))) (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x8) false) (& (bv 16 0xfeff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set swd (| (<< (ite false (bv 16 0x1) (bv 16 0x0)) (bv 8 0xa) false) (& (bv 16 0xfbff) (var swd)))) (set swd (| (<< (ite (! (|| (|| (is_nan (float 2 (var st0) )) (is_nan (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (|| (<. (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (<. (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))) (float 2 (var st0) ))))) (bv 16 0x1) (bv 16 0x0)) (bv 8 0xe) false) (& (bv 16 0xbfff) (var swd)))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fild word [rax]" df00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fild dword [rax]" db00 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fild qword [rax]" df28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 64 (+ (var rax) (bv 64 0x0)))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm))))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
 a "fldcw word [rax]" d928 0x0 (set cwd (loadw 0 16 (+ (var rax) (bv 64 0x0))))
 a "fldenv [rax]" d920
-a "fbld tbyte [rax]" df20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set mem (+ (var rax) (bv 64 0x0))) (set i (bv 64 0x8)) (set val (bv 64 0x0)) (repeat (|| (! (ule (var i) (bv 64 0x0))) (== (var i) (bv 64 0x0))) (seq (set byte (loadw 0 8 (+ (var mem) (var i)))) (set val (+ (* (var val) (bv 64 0x64)) (cast 64 false (+ (* (>> (var byte) (bv 8 0x4) false) (bv 8 0xa)) (& (var byte) (bv 8 0xf)))))) (set i (- (var i) (bv 64 0x1))))) (set f (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var val)) (fcast_sfloat ieee754-bin80 rtz (var val)))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (is_zero (loadw 0 8 (+ (var mem) (bv 64 0x9)))) (var f) (fneg (var f))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fbstp tbyte [rax]" df30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set val (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 64 rne (float 2 (var st0) )) (fcast_sint 64 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set sgn (msb (var val))) (set val (ite (var sgn) (~- (var val)) (var val))) (branch (|| (! (sle (var val) (bv 64 0xde0b6b3a7640000))) (== (var val) (bv 64 0xde0b6b3a7640000))) (goto int) (seq (set mem (+ (var rax) (bv 64 0x0))) (set i (bv 64 0x0)) (repeat (&& (ule (var i) (bv 64 0x9)) (! (== (var i) (bv 64 0x9)))) (seq (storew 0 (+ (var mem) (var i)) (cast 8 false (| (<< (div (mod (var val) (bv 64 0x64)) (bv 64 0xa)) (bv 8 0x4) false) (mod (var val) (bv 64 0xa))))) (set val (div (var val) (bv 64 0x64))) (set i (+ (var i) (bv 64 0x1))))) (set mem (+ (var mem) (var i))) (branch (var sgn) (storew 0 (var mem) (bv 8 0xff)) (storew 0 (var mem) (bv 8 0x0))))))
+a "fbld tbyte [rax]" df20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set mem (+ (var rax) (bv 64 0x0))) (set i (bv 64 0x8)) (set val (bv 64 0x0)) (repeat (|| (! (ule (var i) (bv 64 0x0))) (== (var i) (bv 64 0x0))) (seq (set byte (loadw 0 8 (+ (var mem) (var i)))) (set val (+ (* (var val) (bv 64 0x64)) (cast 64 false (+ (* (>> (var byte) (bv 8 0x4) false) (bv 8 0xa)) (& (var byte) (bv 8 0xf)))))) (set i (- (var i) (bv 64 0x1))))) (set i_val_rm (var val)) (set f (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set swd (| (<< (cast 16 false (- (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st7 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st0) ))) (set st0 (fbits (ite (is_zero (loadw 0 8 (+ (var mem) (bv 64 0x9)))) (var f) (fneg (var f))))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x7)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fbstp tbyte [rax]" df30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st0) )) (set val (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 64 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 64 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 64 rtp (var f_val_rm)) (fcast_sint 64 rtz (var f_val_rm)))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))) (set sgn (msb (var val))) (set val (ite (var sgn) (~- (var val)) (var val))) (branch (|| (! (sle (var val) (bv 64 0xde0b6b3a7640000))) (== (var val) (bv 64 0xde0b6b3a7640000))) (goto int) (seq (set mem (+ (var rax) (bv 64 0x0))) (set i (bv 64 0x0)) (repeat (&& (ule (var i) (bv 64 0x9)) (! (== (var i) (bv 64 0x9)))) (seq (storew 0 (+ (var mem) (var i)) (cast 8 false (| (<< (div (mod (var val) (bv 64 0x64)) (bv 64 0xa)) (bv 8 0x4) false) (mod (var val) (bv 64 0xa))))) (set val (div (var val) (bv 64 0x64))) (set i (+ (var i) (bv 64 0x1))))) (set mem (+ (var mem) (var i))) (branch (var sgn) (storew 0 (var mem) (bv 8 0xff)) (storew 0 (var mem) (bv 8 0x0))))))
 a "fxrstor [rax]" 0fae08
 a "fxsave [rax]" 0fae00
-a "fist word [rax]" df10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 16 rne (float 2 (var st0) )) (fcast_sint 16 rtz (float 2 (var st0) )))))
-a "fist dword [rax]" db10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 32 rne (float 2 (var st0) )) (fcast_sint 32 rtz (float 2 (var st0) )))))
-a "fistp word [rax]" df18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 16 rne (float 2 (var st0) )) (fcast_sint 16 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fistp dword [rax]" db18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 32 rne (float 2 (var st0) )) (fcast_sint 32 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fistp qword [rax]" df38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 64 rne (float 2 (var st0) )) (fcast_sint 64 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fisttp word [rax]" df08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 16 rne (float 2 (var st0) )) (fcast_sint 16 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fisttp dword [rax]" db08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 32 rne (float 2 (var st0) )) (fcast_sint 32 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fisttp qword [rax]" dd08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 64 rne (float 2 (var st0) )) (fcast_sint 64 rtz (float 2 (var st0) )))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fist word [rax]" df10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 16 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 16 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 16 rtp (var f_val_rm)) (fcast_sint 16 rtz (var f_val_rm)))))))
+a "fist dword [rax]" db10 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 32 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 32 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 32 rtp (var f_val_rm)) (fcast_sint 32 rtz (var f_val_rm)))))))
+a "fistp word [rax]" df18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 16 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 16 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 16 rtp (var f_val_rm)) (fcast_sint 16 rtz (var f_val_rm)))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fistp dword [rax]" db18 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 32 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 32 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 32 rtp (var f_val_rm)) (fcast_sint 32 rtz (var f_val_rm)))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fistp qword [rax]" df38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 64 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 64 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 64 rtp (var f_val_rm)) (fcast_sint 64 rtz (var f_val_rm)))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fisttp word [rax]" df08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 16 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 16 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 16 rtp (var f_val_rm)) (fcast_sint 16 rtz (var f_val_rm)))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fisttp dword [rax]" db08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 32 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 32 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 32 rtp (var f_val_rm)) (fcast_sint 32 rtz (var f_val_rm)))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fisttp qword [rax]" dd08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st0) )) (storew 0 (+ (var rax) (bv 64 0x0)) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sint 64 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sint 64 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sint 64 rtp (var f_val_rm)) (fcast_sint 64 rtz (var f_val_rm)))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
 a "fstenv [rcx]" 9bd931
 a "fnstenv [rcx]" d931
-a "fdiv dword[rax]" d830 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))))))))
-a "fdiv qword [rax]" dc30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))))))))
-a "fdiv st0, st7" d8f7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) )))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))))))))
-a "fdiv st6, st0" dcfe 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st6) ) (float 2 (var st6) )) (/. rtz (float 2 (var st6) ) (float 2 (var st6) ))))))
-a "fdivp" def9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st1) ) (float 2 (var st0) )) (/. rtz (float 2 (var st1) ) (float 2 (var st0) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fdivp st2, st0" defa 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st1) ) (float 2 (var st0) )) (/. rtz (float 2 (var st1) ) (float 2 (var st0) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fidiv word [rax]" de30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))))))
-a "fidiv dword [rax]" da30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))) (/. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))))))
-a "fdivr dword[rax]" d838 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (/. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) ))))))
-a "fdivr qword [rax]" dc38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (/. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) ))))))
-a "fdivr st0, st7" d8ff 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))) (float 2 (var st0) )) (/. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))) (float 2 (var st0) ))))))
-a "fdivr st6, st0" dcf6 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st6) ) (float 2 (var st6) )) (/. rtz (float 2 (var st6) ) (float 2 (var st6) ))))))
-a "fdivrp" def1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st1) ) (float 2 (var st0) )) (/. rtz (float 2 (var st1) ) (float 2 (var st0) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fdivrp st2, st0" def2 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (float 2 (var st1) ) (float 2 (var st0) )) (/. rtz (float 2 (var st1) ) (float 2 (var st0) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fidivr word [rax]" de38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (/. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) ))))))
-a "fidivr dword [rax]" da38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (/. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) ))))))
-a "fmul dword[rax]" d808 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (*. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) ))))))
-a "fmul qword [rax]" dc08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (*. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) ))))))
-a "fmul st0, st7" d8cf 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))) (float 2 (var st0) )) (*. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))) (float 2 (var st0) ))))))
-a "fmul st6, st0" dcce 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (float 2 (var st6) ) (float 2 (var st6) )) (*. rtz (float 2 (var st6) ) (float 2 (var st6) ))))))
-a "fmulp" dec9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (float 2 (var st0) ) (float 2 (var st1) )) (*. rtz (float 2 (var st0) ) (float 2 (var st1) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fmulp st2, st0" deca 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (float 2 (var st0) ) (float 2 (var st1) )) (*. rtz (float 2 (var st0) ) (float 2 (var st1) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fimul word [rax]" de08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (*. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) ))))))
-a "fimul dword [rax]" da08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (*. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) ))))))
-a "fsub dword[rax]" d820 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )))) (-. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))))))))
-a "fsub qword [rax]" dc20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )))) (-. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))))))))
-a "fsub st0, st7" d8e7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) )))) (-. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))))))))
-a "fsub st6, st0" dcee 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st6) ) (float 2 (var st6) )) (-. rtz (float 2 (var st6) ) (float 2 (var st6) ))))))
-a "fsubp" dee9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st1) ) (float 2 (var st0) )) (-. rtz (float 2 (var st1) ) (float 2 (var st0) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fsubp st2, st0" deea 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st1) ) (float 2 (var st0) )) (-. rtz (float 2 (var st1) ) (float 2 (var st0) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fisub word [rax]" de20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0)))))) (-. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))))))))
-a "fisub dword [rax]" da20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0)))))) (-. rtz (float 2 (var st0) ) (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))))))))
-a "fsubr dword[rax]" d828 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (-. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) ))))))
-a "fsubr qword [rax]" dc28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) )) (-. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (fconvert ieee754-bin80 rtz (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) ))) (float 2 (var st0) ))))))
-a "fsubr st0, st7" d8ef 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))) (float 2 (var st0) )) (-. rtz (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (float 2 (var st7) )) (fconvert ieee754-bin80 rtz (float 2 (var st7) ))) (float 2 (var st0) ))))))
-a "fsubr st6, st0" dce6 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st6) ) (float 2 (var st6) )) (-. rtz (float 2 (var st6) ) (float 2 (var st6) ))))))
-a "fsubrp" dee1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (float 2 (var st1) )) (-. rtz (float 2 (var st0) ) (float 2 (var st1) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fsubrp st2, st0" dee2 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (float 2 (var st0) ) (float 2 (var st1) )) (-. rtz (float 2 (var st0) ) (float 2 (var st1) ))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
-a "fisubr word [rax]" de28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (-. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 16 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) ))))))
-a "fisubr dword [rax]" da28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) )) (-. rtz (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (fcast_sfloat ieee754-bin80 rtz (loadw 0 32 (+ (var rax) (bv 64 0x0))))) (float 2 (var st0) ))))))
+a "fdiv dword[rax]" d830 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fdiv qword [rax]" dc30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fdiv st0, st7" d8f7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fdiv st6, st0" dcfe 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st6) )) (set y_rm (float 2 (var st6) )) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fdivp" def9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fdivp st2, st0" defa 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fidiv word [rax]" de30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fidiv dword [rax]" da30 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fdivr dword[rax]" d838 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fdivr qword [rax]" dc38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fdivr st0, st7" d8ff 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fdivr st6, st0" dcf6 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st6) )) (set y_rm (float 2 (var st6) )) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fdivrp" def1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fdivrp st2, st0" def2 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fidivr word [rax]" de38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fidivr dword [rax]" da38 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (/. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (/. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (/. rtp (var x_rm) (var y_rm)) (/. rtz (var x_rm) (var y_rm))))))))
+a "fmul dword[rax]" d808 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
+a "fmul qword [rax]" dc08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
+a "fmul st0, st7" d8cf 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
+a "fmul st6, st0" dcce 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st6) )) (set y_rm (float 2 (var st6) )) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
+a "fmulp" dec9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fmulp st2, st0" deca 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fimul word [rax]" de08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
+a "fimul dword [rax]" da08 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (*. rne (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x1)) (*. rtn (var x_rm) (var y_rm)) (ite (== (var _rmode) (bv 2 0x2)) (*. rtp (var x_rm) (var y_rm)) (*. rtz (var x_rm) (var y_rm))))))))
+a "fsub dword[rax]" d820 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
+a "fsub qword [rax]" dc20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
+a "fsub st0, st7" d8e7 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
+a "fsub st6, st0" dcee 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st6) )) (set y_rm (float 2 (var st6) )) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
+a "fsubp" dee9 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fsubp st2, st0" deea 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st0) )) (set y_rm (float 2 (var st1) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fisub word [rax]" de20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
+a "fisub dword [rax]" da20 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set x_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set y_rm (float 2 (var st0) )) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
+a "fsubr dword[rax]" d828 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 0 (loadw 0 32 (+ (var rax) (bv 64 0x0))) )) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
+a "fsubr qword [rax]" dc28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 1 (loadw 0 64 (+ (var rax) (bv 64 0x0))) )) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
+a "fsubr st0, st7" d8ef 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set f_val_rm (float 2 (var st7) )) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fconvert ieee754-bin80 rne (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fconvert ieee754-bin80 rtn (var f_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fconvert ieee754-bin80 rtp (var f_val_rm)) (fconvert ieee754-bin80 rtz (var f_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
+a "fsubr st6, st0" dce6 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st6) )) (set y_rm (float 2 (var st6) )) (set st6 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
+a "fsubrp" dee1 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st1) )) (set y_rm (float 2 (var st0) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fsubrp st2, st0" dee2 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set x_rm (float 2 (var st1) )) (set y_rm (float 2 (var st0) )) (set st1 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))) (set swd (| (<< (cast 16 false (+ (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x1))) (bv 8 0xb) false) (& (bv 16 0xc7ff) (var swd)))) (set st0 (fbits (float 2 (var st1) ))) (set st1 (fbits (float 2 (var st2) ))) (set st2 (fbits (float 2 (var st3) ))) (set st3 (fbits (float 2 (var st4) ))) (set st4 (fbits (float 2 (var st5) ))) (set st5 (fbits (float 2 (var st6) ))) (set st6 (fbits (float 2 (var st7) ))) (set swd (| (<< (ite (== (cast 3 false (>> (var swd) (bv 8 0xb) false)) (bv 3 0x0)) (bv 16 0x1) (bv 16 0x0)) (bv 8 0x9) false) (& (bv 16 0xfdff) (var swd)))))
+a "fisubr word [rax]" de28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 16 (+ (var rax) (bv 64 0x0)))) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
+a "fisubr dword [rax]" da28 0x0 (seq (set _rmode (cast 2 false (>> (var cwd) (bv 8 0xa) false))) (set i_val_rm (loadw 0 32 (+ (var rax) (bv 64 0x0)))) (set x_rm (float 2 (var st0) )) (set y_rm (ite (== (var _rmode) (bv 2 0x0)) (fcast_sfloat ieee754-bin80 rne (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x1)) (fcast_sfloat ieee754-bin80 rtn (var i_val_rm)) (ite (== (var _rmode) (bv 2 0x2)) (fcast_sfloat ieee754-bin80 rtp (var i_val_rm)) (fcast_sfloat ieee754-bin80 rtz (var i_val_rm)))))) (set st0 (fbits (ite (== (var _rmode) (bv 2 0x0)) (-. rne (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x1)) (-. rtn (var y_rm) (var x_rm)) (ite (== (var _rmode) (bv 2 0x2)) (-. rtp (var y_rm) (var x_rm)) (-. rtz (var y_rm) (var x_rm))))))))
 # Not testing [fstcw] and [fstsw] since they are made up of a [wait] instruction and a [fnstcw] (or [fnstsw]) instruction, and we already test both of these instructions.
 a "fstcw word [rcx]" 9bd939
 a "fnstcw word [rcx]" d939 0x0 (storew 0 (+ (var rcx) (bv 64 0x0)) (var cwd))