diff --git a/ir/state.cpp b/ir/state.cpp
index 8fd14c42f..032ab83ad 100644
--- a/ir/state.cpp
+++ b/ir/state.cpp
@@ -255,7 +255,11 @@ State::State(const Function &f, bool source)
   : f(f), source(source), memory(*this),
     fp_rounding_mode(expr::mkVar("fp_rounding_mode", 3)),
     fp_denormal_mode(expr::mkVar("fp_denormal_mode", 2)),
-    return_val(DisjointExpr(f.getType().getDummyValue(false))) {}
+    return_val(DisjointExpr(f.getType().getDummyValue(false))) {
+
+  if (get_uf_float())
+    doesApproximation("uf-float");
+}
 
 void State::resetGlobals() {
   Memory::resetGlobals();
diff --git a/ir/type.cpp b/ir/type.cpp
index ee7c1e805..8059bd0fb 100644
--- a/ir/type.cpp
+++ b/ir/type.cpp
@@ -5,6 +5,7 @@
 #include "ir/globals.h"
 #include "ir/state.h"
 #include "smt/solver.h"
+#include "smt/smt.h"
 #include "util/compiler.h"
 #include <array>
 #include <cassert>
@@ -450,7 +451,7 @@ expr FloatType::fromFloat(State &s, const expr &fp, const Type &from_type0,
   expr isnan = fp.isNaN();
   expr val = fp.float2BV();
 
-  if (isnan.isFalse())
+  if (isnan.isFalse() || get_uf_float())
     return val;
 
   unsigned fraction_bits = fractionBits();
diff --git a/llvm_util/cmd_args_def.h b/llvm_util/cmd_args_def.h
index f1c473df5..3b5fba6f0 100644
--- a/llvm_util/cmd_args_def.h
+++ b/llvm_util/cmd_args_def.h
@@ -23,6 +23,7 @@ smt::solver_tactic_verbose(opt_tactic_verbose);
 config::debug = opt_debug;
 config::max_offset_bits = opt_max_offset_in_bits;
 config::max_sizet_bits  = opt_max_sizet_in_bits;
+smt::set_uf_float(opt_uf_float);
 
 if ((config::disallow_ub_exploitation = opt_disallow_ub_exploitation)) {
   config::disable_undef_input = true;
diff --git a/llvm_util/cmd_args_list.h b/llvm_util/cmd_args_list.h
index b732ec92a..c70689c2a 100644
--- a/llvm_util/cmd_args_list.h
+++ b/llvm_util/cmd_args_list.h
@@ -185,4 +185,9 @@ llvm::cl::opt<bool> opt_disallow_ub_exploitation(
   llvm::cl::desc("Disallow UB exploitation by optimizations (default=allow)"),
   llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));
 
+llvm::cl::opt<bool> opt_uf_float(
+  LLVM_ARGS_PREFIX "uf-float",
+  llvm::cl::desc("Encode floating point operations using uninterpreted functions"),
+  llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));
+
 }
diff --git a/smt/expr.cpp b/smt/expr.cpp
index 70353e8a1..24c0e2572 100644
--- a/smt/expr.cpp
+++ b/smt/expr.cpp
@@ -4,6 +4,7 @@
 #include "smt/expr.h"
 #include "smt/exprs.h"
 #include "smt/ctx.h"
+#include "smt/smt.h"
 #include "util/compiler.h"
 #include <algorithm>
 #include <bit>
@@ -12,6 +13,7 @@
 #include <limits>
 #include <memory>
 #include <string>
+#include <sstream>
 #include <z3.h>
 
 #define DEBUG_Z3_RC 0
@@ -218,13 +220,20 @@ expr expr::mkInt(const char *n, unsigned bits) {
   return bits ? Z3_mk_numeral(ctx(), n, mkBVSort(bits)) : expr();
 }
 
+static expr to_uf_float_sort(expr&& e) {
+  if (get_uf_float() && e.isFloat())
+    return e.float2BV();
+  return e;
+}
+
 expr expr::mkFloat(double n, const expr &type) {
   C2(type);
-  return Z3_mk_fpa_numeral_double(ctx(), n, type.sort());
+  return to_uf_float_sort(Z3_mk_fpa_numeral_double(ctx(), n, type.sort()));
 }
 
 expr expr::mkHalf(float n) {
-  return Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_half(ctx()));
+  return to_uf_float_sort(
+    Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_half(ctx())));
 }
 
 static Z3_sort mk_bfloat_sort() {
@@ -232,29 +241,32 @@ static Z3_sort mk_bfloat_sort() {
 }
 
 expr expr::mkBFloat(float n) {
-  return Z3_mk_fpa_numeral_float(ctx(), n, mk_bfloat_sort());
+  return to_uf_float_sort(Z3_mk_fpa_numeral_float(ctx(), n, mk_bfloat_sort()));
 }
 
 expr expr::mkFloat(float n) {
-  return Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_single(ctx()));
+  return to_uf_float_sort(
+    Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_single(ctx())));
 }
 
 expr expr::mkDouble(double n) {
-  return Z3_mk_fpa_numeral_double(ctx(), n, Z3_mk_fpa_sort_double(ctx()));
+  return to_uf_float_sort(
+    Z3_mk_fpa_numeral_double(ctx(), n, Z3_mk_fpa_sort_double(ctx())));
 }
 
 expr expr::mkQuad(double n) {
-  return Z3_mk_fpa_numeral_double(ctx(), n, Z3_mk_fpa_sort_quadruple(ctx()));
+  return to_uf_float_sort(
+    Z3_mk_fpa_numeral_double(ctx(), n, Z3_mk_fpa_sort_quadruple(ctx())));
 }
 
 expr expr::mkNaN(const expr &type) {
   C2(type);
-  return Z3_mk_fpa_nan(ctx(), type.sort());
+  return to_uf_float_sort(Z3_mk_fpa_nan(ctx(), type.sort()));
 }
 
 expr expr::mkNumber(const char *n, const expr &type) {
   C2(type);
-  return Z3_mk_numeral(ctx(), n, type.sort());
+  return to_uf_float_sort(Z3_mk_numeral(ctx(), n, type.sort()));
 }
 
 expr expr::mkConst(Z3_decl decl) {
@@ -1136,7 +1148,44 @@ expr expr::round_up(const expr &power_of_two) const {
     return v.fn();                                       \
 } while (0)
 
+static expr uf_float(const char *prefix, vector<expr> args,
+                     const expr &range, bool is_commutative = false) {
+  ostringstream os;
+  os << prefix;
+  for (const expr& arg : args) {
+    os << '.';
+    arg.printSort(os);
+  }
+  os << '.';
+  range.printSort(os);
+
+  string name = std::move(os).str();
+  expr uf = expr::mkUF(name, args, range);
+  if (is_commutative) {
+    assert(args.size() >= 2);
+    assert(range.isBV() || range.isBool());
+    assert(args[0].isSameTypeOf(args[1]));
+
+    // Commutative functions are encoded as
+    //   op(x, y) = op'(x, y) & op'(y, x)
+    // where & is the bitwise and operator and op' is an uninterpreted function.
+    // This encoding comes from "SMT-based Translation Validation for Machine
+    // Learning Compiler" by Seongwon Bang, Seunghyeon Nam, Inwhan Chun,
+    // Ho Young Jhoo, and Juneyoung Lee
+
+    swap(args[0], args[1]);
+    expr uf2 = expr::mkUF(name, args, range);
+    if (range.isBool())
+      return uf && uf2;
+    return uf & uf2;
+  }
+  return uf;
+}
+
 expr expr::isNaN() const {
+  if (get_uf_float())
+    return uf_float("isNaN", {*this}, true);
+  
   fold_fp_neg(isNaN);
 
   expr v;
@@ -1147,6 +1196,9 @@ expr expr::isNaN() const {
 }
 
 expr expr::isInf() const {
+  if (get_uf_float())
+    return uf_float("isInf", {*this}, true);
+  
   fold_fp_neg(isInf);
 
   expr v;
@@ -1159,10 +1211,14 @@ expr expr::isInf() const {
 expr expr::isFPZero() const {
   if (isBV())
     return extract(bits()-2, 0) == 0;
+  if (get_uf_float())
+    return uf_float("isFPZero", {*this}, true);
   return unop_fold(Z3_mk_fpa_is_zero);
 }
 
 expr expr::isFPNegative() const {
+  if (get_uf_float())
+    return uf_float("isFPNegative", {*this}, true);
   return unop_fold(Z3_mk_fpa_is_negative);
 }
 
@@ -1171,10 +1227,14 @@ expr expr::isFPNegZero() const {
 }
 
 expr expr::isFPNormal() const {
+  if (get_uf_float())
+    return uf_float("isFPNormal", {*this}, true);
   return unop_fold(Z3_mk_fpa_is_normal);
 }
 
 expr expr::isFPSubNormal() const {
+  if (get_uf_float())
+    return uf_float("isFPSubNormal", {*this}, true);
   return unop_fold(Z3_mk_fpa_is_subnormal);
 }
 
@@ -1200,26 +1260,36 @@ expr expr::rtz() {
 
 expr expr::fadd(const expr &rhs, const expr &rm) const {
   C(rhs, rm);
+  if (get_uf_float())
+    return uf_float("fadd", {*this, rhs, rm}, *this, true);
   return simplify_const(Z3_mk_fpa_add(ctx(), rm(), ast(), rhs()), *this, rhs);
 }
 
 expr expr::fsub(const expr &rhs, const expr &rm) const {
   C(rhs, rm);
+  if (get_uf_float())
+    return uf_float("fsub", {*this, rhs, rm}, *this);
   return simplify_const(Z3_mk_fpa_sub(ctx(), rm(), ast(), rhs()), *this, rhs);
 }
 
 expr expr::fmul(const expr &rhs, const expr &rm) const {
   C(rhs, rm);
+  if (get_uf_float())
+    return uf_float("fmul", {*this, rhs, rm}, *this, true);
   return simplify_const(Z3_mk_fpa_mul(ctx(), rm(), ast(), rhs()), *this, rhs);
 }
 
 expr expr::fdiv(const expr &rhs, const expr &rm) const {
   C(rhs, rm);
+  if (get_uf_float())
+    return uf_float("fdiv", {*this, rhs, rm}, *this);
   return simplify_const(Z3_mk_fpa_div(ctx(), rm(), ast(), rhs()), *this, rhs);
 }
 
 expr expr::frem(const expr &rhs) const {
   C(rhs);
+  if (get_uf_float())
+    return uf_float("frem", {*this, rhs}, *this);
   return simplify_const(Z3_mk_fpa_rem(ctx(), ast(), rhs()), *this, rhs);
 }
 
@@ -1227,6 +1297,9 @@ expr expr::fabs() const {
   if (isBV())
     return mkUInt(0, 1).concat(extract(bits() - 2, 0));
 
+  if (get_uf_float())
+    return uf_float("fabs", {*this}, *this);
+
   fold_fp_neg(fabs);
   return unop_fold(Z3_mk_fpa_abs);
 }
@@ -1237,6 +1310,10 @@ expr expr::fneg() const {
     return (extract(signbit, signbit) ^ mkUInt(1, 1))
              .concat(extract(signbit - 1, 0));
   }
+
+  if (get_uf_float())
+    return uf_float("fneg", {*this}, *this);
+  
   return unop_fold(Z3_mk_fpa_neg);
 }
 
@@ -1247,11 +1324,15 @@ expr expr::copysign(const expr &sign) const {
 
 expr expr::sqrt(const expr &rm) const {
   C(rm);
+  if (get_uf_float())
+    return uf_float("sqrt", {*this, rm}, *this);
   return simplify_const(Z3_mk_fpa_sqrt(ctx(), rm(), ast()), *this);
 }
 
 expr expr::fma(const expr &a, const expr &b, const expr &c, const expr &rm) {
   C2(a, b, c, rm);
+  if (get_uf_float())
+    return uf_float("fma", {a, b, c, rm}, a);
   return simplify_const(Z3_mk_fpa_fma(ctx(), rm(), a(), b(), c()), a, b, c);
 }
 
@@ -1265,32 +1346,38 @@ expr expr::floor() const {
 
 expr expr::round(const expr &rm) const {
   C(rm);
+  if (get_uf_float())
+    return uf_float("round", {*this, rm}, *this);
   return
     simplify_const(Z3_mk_fpa_round_to_integral(ctx(), rm(), ast()), *this);
 }
 
 expr expr::foeq(const expr &rhs) const {
+  if (get_uf_float())
+    return uf_float("foeq", {*this, rhs}, true, true);
   return binop_commutative(rhs, Z3_mk_fpa_eq);
 }
 
 expr expr::fogt(const expr &rhs) const {
-  return binop_fold(rhs, Z3_mk_fpa_gt);
+  return rhs.folt(*this);
 }
 
 expr expr::foge(const expr &rhs) const {
-  return binop_fold(rhs, Z3_mk_fpa_geq);
+  return !fult(rhs);
 }
 
 expr expr::folt(const expr &rhs) const {
+  if (get_uf_float())
+    return uf_float("folt", {*this, rhs}, true);
   return binop_fold(rhs, Z3_mk_fpa_lt);
 }
 
 expr expr::fole(const expr &rhs) const {
-  return binop_fold(rhs, Z3_mk_fpa_leq);
+  return rhs.foge(*this);
 }
 
 expr expr::fone(const expr &rhs) const {
-  return ford(rhs) && !binop_commutative(rhs, Z3_mk_fpa_eq);
+  return !fueq(rhs);
 }
 
 expr expr::ford(const expr &rhs) const {
@@ -1298,27 +1385,31 @@ expr expr::ford(const expr &rhs) const {
 }
 
 expr expr::fueq(const expr &rhs) const {
+  if (get_uf_float())
+    return uf_float("fueq", {*this, rhs}, true, true);
   return funo(rhs) || binop_commutative(rhs, Z3_mk_fpa_eq);
 }
 
 expr expr::fugt(const expr &rhs) const {
-  return funo(rhs) || binop_fold(rhs, Z3_mk_fpa_gt);
+  return rhs.fult(*this);
 }
 
 expr expr::fuge(const expr &rhs) const {
-  return funo(rhs) || binop_fold(rhs, Z3_mk_fpa_geq);
+  return !folt(rhs);
 }
 
 expr expr::fult(const expr &rhs) const {
+  if (get_uf_float())
+    return uf_float("fult", {*this, rhs}, true);
   return funo(rhs) || binop_fold(rhs, Z3_mk_fpa_lt);
 }
 
 expr expr::fule(const expr &rhs) const {
-  return funo(rhs) || binop_fold(rhs, Z3_mk_fpa_leq);
+  return rhs.fuge(*this);
 }
 
 expr expr::fune(const expr &rhs) const {
-  return funo(rhs) || !binop_commutative(rhs, Z3_mk_fpa_eq);
+  return !foeq(rhs);
 }
 
 expr expr::funo(const expr &rhs) const {
@@ -1925,6 +2016,9 @@ expr expr::toBVBool() const {
 }
 
 expr expr::float2BV() const {
+  if (isBV())
+    return *this;
+  
   if (auto app = isAppOf(Z3_OP_FPA_TO_FP)) // ((_ to_fp e s) BV)
     if (Z3_get_app_num_args(ctx(), app) == 1)
       return Z3_get_app_arg(ctx(), app, 0);
@@ -1938,6 +2032,9 @@ expr expr::float2Real() const {
 
 expr expr::BV2float(const expr &type) const {
   C(type);
+  if (get_uf_float())
+    return *this; 
+  
   if (auto app = isAppOf(Z3_OP_FPA_TO_IEEE_BV)) {
     expr arg = Z3_get_app_arg(ctx(), app, 0);
     if (arg.sort() == type.sort())
@@ -1949,28 +2046,38 @@ expr expr::BV2float(const expr &type) const {
 
 expr expr::float2Float(const expr &type, const expr &rm) const {
   C(type, rm);
+  if (get_uf_float())
+    return uf_float("float2Float", {*this, rm}, type);
   return simplify_const(Z3_mk_fpa_to_fp_float(ctx(), rm(), ast(), type.sort()),
                         *this);
 }
 
 expr expr::fp2sint(unsigned bits, const expr &rm) const {
   C(rm);
+  if (get_uf_float())
+    return uf_float("fp2sint", {*this, rm}, expr::mkUInt(0, bits));
   return simplify_const(Z3_mk_fpa_to_sbv(ctx(), rm(), ast(), bits), *this);
 }
 
 expr expr::fp2uint(unsigned bits, const expr &rm) const {
   C(rm);
+  if (get_uf_float())
+    return uf_float("fp2uint", {*this, rm}, expr::mkUInt(0, bits));
   return simplify_const(Z3_mk_fpa_to_ubv(ctx(), rm(), ast(), bits), *this);
 }
 
 expr expr::sint2fp(const expr &type, const expr &rm) const {
   C(type, rm);
+  if (get_uf_float())
+    return uf_float("sint2fp", {*this, rm}, type);
   return simplify_const(Z3_mk_fpa_to_fp_signed(ctx(), rm(), ast(), type.sort()),
                         *this);
 }
 
 expr expr::uint2fp(const expr &type, const expr &rm) const {
   C(type, rm);
+  if (get_uf_float())
+    return uf_float("uint2fp", {*this, rm}, type);
   return
     simplify_const(Z3_mk_fpa_to_fp_unsigned(ctx(), rm(), ast(), type.sort()),
                    *this);
@@ -2328,6 +2435,10 @@ void expr::printHexadecimal(ostream &os) const {
   os << (rem == 0 ? *this : zext(4 - rem));
 }
 
+void expr::printSort(ostream &os) const {
+  os << Z3_sort_to_string(ctx(), sort());
+}
+
 string expr::numeral_string() const {
   C();
   return Z3_get_numeral_decimal_string(ctx(), ast(), 12);
diff --git a/smt/expr.h b/smt/expr.h
index 038613e7c..ce9d0b821 100644
--- a/smt/expr.h
+++ b/smt/expr.h
@@ -370,6 +370,7 @@ class expr {
   void printUnsigned(std::ostream &os) const;
   void printSigned(std::ostream &os) const;
   void printHexadecimal(std::ostream &os) const;
+  void printSort(std::ostream &os) const;
   std::string numeral_string() const;
   std::string fn_name() const; // empty if not a function
   unsigned getFnNumArgs() const;
diff --git a/smt/smt.cpp b/smt/smt.cpp
index 1f72aeb8b..7bb396072 100644
--- a/smt/smt.cpp
+++ b/smt/smt.cpp
@@ -42,6 +42,7 @@ void smt_initializer::destroy() {
 
 static string query_timeout = "10000";
 static string rand_seed = "0";
+static bool uf_float = false;
 
 void set_query_timeout(string ms) {
   query_timeout = std::move(ms);
@@ -59,6 +60,14 @@ const char *get_random_seed() {
   return rand_seed.c_str();
 }
 
+void set_uf_float(bool enable) {
+  uf_float = enable;
+}
+
+bool get_uf_float() {
+  return uf_float;
+}
+
 
 static uint64_t z3_memory_limit = 1ull << 30; // 1 GB
 
diff --git a/smt/smt.h b/smt/smt.h
index a33390539..f340e5348 100644
--- a/smt/smt.h
+++ b/smt/smt.h
@@ -23,6 +23,8 @@ void set_query_timeout(std::string ms);
 const char* get_query_timeout();
 void set_random_seed(std::string seed);
 const char *get_random_seed();
+void set_uf_float(bool enable);
+bool get_uf_float();
 
 void set_memory_limit(uint64_t limit);
 bool hit_memory_limit();
diff --git a/tests/alive-tv/uf-float/add-assoc-fail.srctgt.ll b/tests/alive-tv/uf-float/add-assoc-fail.srctgt.ll
new file mode 100644
index 000000000..33a3d5323
--- /dev/null
+++ b/tests/alive-tv/uf-float/add-assoc-fail.srctgt.ll
@@ -0,0 +1,14 @@
+; TEST-ARGS: --uf-float
+; ERROR: Couldn't prove the correctness of the transformation
+
+define float @src(float noundef %x, float noundef %y, float noundef %z) {
+  %a = fadd float %x, %y
+  %b = fadd float %a, %z
+  ret float %b
+}
+
+define float @tgt(float noundef %x, float noundef %y, float noundef %z) {
+  %a = fadd float %y, %z
+  %b = fadd float %x, %a
+  ret float %b
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/add-comm-double.srctgt.ll b/tests/alive-tv/uf-float/add-comm-double.srctgt.ll
new file mode 100644
index 000000000..4981661a4
--- /dev/null
+++ b/tests/alive-tv/uf-float/add-comm-double.srctgt.ll
@@ -0,0 +1,11 @@
+; TEST-ARGS: --uf-float
+
+define double @src(double noundef %x, double noundef %y) {
+  %sum = fadd double %x, %y
+  ret double %sum
+}
+
+define double @tgt(double noundef %x, double noundef %y) {
+  %sum = fadd double %y, %x
+  ret double %sum
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/add-comm-fp128.srctgt.ll b/tests/alive-tv/uf-float/add-comm-fp128.srctgt.ll
new file mode 100644
index 000000000..deb6c3213
--- /dev/null
+++ b/tests/alive-tv/uf-float/add-comm-fp128.srctgt.ll
@@ -0,0 +1,11 @@
+; TEST-ARGS: --uf-float
+
+define fp128 @src(fp128 noundef %x, fp128 noundef %y) {
+  %sum = fadd fp128 %x, %y
+  ret fp128 %sum
+}
+
+define fp128 @tgt(fp128 noundef %x, fp128 noundef %y) {
+  %sum = fadd fp128 %y, %x
+  ret fp128 %sum
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/add-comm-half.srctgt.ll b/tests/alive-tv/uf-float/add-comm-half.srctgt.ll
new file mode 100644
index 000000000..731eae0d5
--- /dev/null
+++ b/tests/alive-tv/uf-float/add-comm-half.srctgt.ll
@@ -0,0 +1,11 @@
+; TEST-ARGS: --uf-float
+
+define half @src(half noundef %x, half noundef %y) {
+  %sum = fadd half %x, %y
+  ret half %sum
+}
+
+define half @tgt(half noundef %x, half noundef %y) {
+  %sum = fadd half %y, %x
+  ret half %sum
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/add-comm-ninf.srctgt.ll b/tests/alive-tv/uf-float/add-comm-ninf.srctgt.ll
new file mode 100644
index 000000000..c52c7779c
--- /dev/null
+++ b/tests/alive-tv/uf-float/add-comm-ninf.srctgt.ll
@@ -0,0 +1,11 @@
+; TEST-ARGS: --uf-float
+
+define float @src(float noundef %x, float noundef %y) {
+  %sum = fadd ninf float %x, %y
+  ret float %sum
+}
+
+define float @tgt(float noundef %x, float noundef %y) {
+  %sum = fadd ninf float %y, %x
+  ret float %sum
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/add-comm-nnan.srctgt.ll b/tests/alive-tv/uf-float/add-comm-nnan.srctgt.ll
new file mode 100644
index 000000000..50d7a7c7e
--- /dev/null
+++ b/tests/alive-tv/uf-float/add-comm-nnan.srctgt.ll
@@ -0,0 +1,11 @@
+; TEST-ARGS: --uf-float
+
+define float @src(float noundef %x, float noundef %y) {
+  %sum = fadd nnan float %x, %y
+  ret float %sum
+}
+
+define float @tgt(float noundef %x, float noundef %y) {
+  %sum = fadd nnan float %y, %x
+  ret float %sum
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/add-comm.srctgt.ll b/tests/alive-tv/uf-float/add-comm.srctgt.ll
new file mode 100644
index 000000000..7f9fa9728
--- /dev/null
+++ b/tests/alive-tv/uf-float/add-comm.srctgt.ll
@@ -0,0 +1,11 @@
+; TEST-ARGS: --uf-float
+
+define float @src(float noundef %x, float noundef %y) {
+  %sum = fadd float %x, %y
+  ret float %sum
+}
+
+define float @tgt(float noundef %x, float noundef %y) {
+  %sum = fadd float %y, %x
+  ret float %sum
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll b/tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll
new file mode 100644
index 000000000..573ade1a4
--- /dev/null
+++ b/tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll
@@ -0,0 +1,11 @@
+; TEST-ARGS: --uf-float
+
+define i1 @src(float noundef %x, float noundef %y) {
+  %cmp = fcmp oeq float %x, %y
+  ret i1 %cmp
+}
+
+define i1 @tgt(float noundef %x, float noundef %y) {
+  %cmp = fcmp oeq float %y, %x
+  ret i1 %cmp
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll b/tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll
new file mode 100644
index 000000000..779b655e0
--- /dev/null
+++ b/tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll
@@ -0,0 +1,12 @@
+; TEST-ARGS: --uf-float
+
+define i1 @src(float noundef %x, float noundef %y) {
+  %cmp = fcmp oeq float %x, %y
+  ret i1 %cmp
+}
+
+define i1 @tgt(float noundef %x, float noundef %y) {
+  %cmp = fcmp une float %x, %y
+  %notcmp = xor i1 %cmp, 1
+  ret i1 %notcmp
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll b/tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll
new file mode 100644
index 000000000..4b3ccdbbb
--- /dev/null
+++ b/tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll
@@ -0,0 +1,11 @@
+; TEST-ARGS: --uf-float
+
+define i1 @src(float noundef %x, float noundef %y) {
+  %cmp = fcmp olt float %x, %y
+  ret i1 %cmp
+}
+
+define i1 @tgt(float noundef %x, float noundef %y) {
+  %cmp = fcmp ogt float %y, %x
+  ret i1 %cmp
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll b/tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll
new file mode 100644
index 000000000..ad124452e
--- /dev/null
+++ b/tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll
@@ -0,0 +1,12 @@
+; TEST-ARGS: --uf-float
+
+define i1 @src(float noundef %x, float noundef %y) {
+  %cmp = fcmp olt float %x, %y
+  ret i1 %cmp
+}
+
+define i1 @tgt(float noundef %x, float noundef %y) {
+  %cmp = fcmp ule float %y, %x
+  %notcmp = xor i1 %cmp, 1
+  ret i1 %notcmp
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/cmp-olt-ult-fail.srctgt.ll b/tests/alive-tv/uf-float/cmp-olt-ult-fail.srctgt.ll
new file mode 100644
index 000000000..b9f92c905
--- /dev/null
+++ b/tests/alive-tv/uf-float/cmp-olt-ult-fail.srctgt.ll
@@ -0,0 +1,12 @@
+; TEST-ARGS: --uf-float
+; ERROR: Couldn't prove the correctness of the transformation
+
+define i1 @src(float noundef %x, float noundef %y) {
+  %cmp = fcmp olt float %x, %y
+  ret i1 %cmp
+}
+
+define i1 @tgt(float noundef %x, float noundef %y) {
+  %cmp = fcmp ult float %x, %y
+  ret i1 %cmp
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll b/tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll
new file mode 100644
index 000000000..9e0d7a0fd
--- /dev/null
+++ b/tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll
@@ -0,0 +1,12 @@
+; TEST-ARGS: --uf-float
+
+define i1 @src(float noundef %x, float noundef %y) {
+  %cmp = fcmp ord float %x, %y
+  %notcmp = xor i1 %cmp, 1
+  ret i1 %notcmp
+}
+
+define i1 @tgt(float noundef %x, float noundef %y) {
+  %cmp = fcmp uno float %y, %x
+  ret i1 %cmp
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/load-bitcast.srctgt.ll b/tests/alive-tv/uf-float/load-bitcast.srctgt.ll
new file mode 100644
index 000000000..8ec87e261
--- /dev/null
+++ b/tests/alive-tv/uf-float/load-bitcast.srctgt.ll
@@ -0,0 +1,13 @@
+; TEST-ARGS: --uf-float
+
+define i32 @src(float noundef %x) {
+  %a = bitcast float %x to i32
+  ret i32 %a
+}
+
+define i32 @tgt(float noundef %x) {
+  %a = alloca float
+  store float %x, ptr %a
+  %b = load i32, ptr %a
+  ret i32 %b
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/load-store.srctgt.ll b/tests/alive-tv/uf-float/load-store.srctgt.ll
new file mode 100644
index 000000000..1c397c404
--- /dev/null
+++ b/tests/alive-tv/uf-float/load-store.srctgt.ll
@@ -0,0 +1,12 @@
+; TEST-ARGS: --uf-float
+
+define float @src(float noundef %x) {
+  ret float %x
+}
+
+define float @tgt(float noundef %x) {
+  %a = alloca float
+  store float %x, ptr %a
+  %b = load float, ptr %a
+  ret float %b
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/select.srctgt.ll b/tests/alive-tv/uf-float/select.srctgt.ll
new file mode 100644
index 000000000..2dcc46005
--- /dev/null
+++ b/tests/alive-tv/uf-float/select.srctgt.ll
@@ -0,0 +1,17 @@
+; TEST-ARGS: --uf-float
+
+define float @src(float noundef %x, float noundef %y) {
+  %cmp = fcmp olt float %x, %y
+  %a = fsub float %y, %x
+  %b = fsub float %x, %y
+  %c = select i1 %cmp, float %a, float %b
+  ret float %c
+}
+
+define float @tgt(float noundef %x, float noundef %y) {
+  %cmp = fcmp olt float %x, %y
+  %min = select i1 %cmp, float %x, float %y
+  %max = select i1 %cmp, float %y, float %x
+  %res = fsub float %max, %min
+  ret float %res
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/vector-binop.srctgt.ll b/tests/alive-tv/uf-float/vector-binop.srctgt.ll
new file mode 100644
index 000000000..98c599077
--- /dev/null
+++ b/tests/alive-tv/uf-float/vector-binop.srctgt.ll
@@ -0,0 +1,14 @@
+; TEST-ARGS: --uf-float
+
+define float @src(float noundef %x, float noundef %y) {
+  %sum = fadd float %x, %y
+  ret float %sum
+}
+
+define float @tgt(float noundef %x, float noundef %y) {
+  %vec1 = insertelement <2 x float> poison, float %x, i32 0
+  %vec2 = insertelement <2 x float> poison, float %y, i32 0
+  %vec3 = fadd <2 x float> %vec1, %vec2
+  %sum = extractelement <2 x float> %vec3, i32 0
+  ret float %sum
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/vector-cmp.srctgt.ll b/tests/alive-tv/uf-float/vector-cmp.srctgt.ll
new file mode 100644
index 000000000..ddc62145b
--- /dev/null
+++ b/tests/alive-tv/uf-float/vector-cmp.srctgt.ll
@@ -0,0 +1,14 @@
+; TEST-ARGS: --uf-float
+
+define i1 @src(float noundef %x, float noundef %y) {
+  %res = fcmp olt float %x, %y
+  ret i1 %res
+}
+
+define i1 @tgt(float noundef %x, float noundef %y) {
+  %vec1 = insertelement <2 x float> poison, float %x, i32 0
+  %vec2 = insertelement <2 x float> poison, float %y, i32 0
+  %vec3 = fcmp olt <2 x float> %vec1, %vec2
+  %res = extractelement <2 x i1> %vec3, i32 0
+  ret i1 %res
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/vector-convert.srctgt.ll b/tests/alive-tv/uf-float/vector-convert.srctgt.ll
new file mode 100644
index 000000000..05636d146
--- /dev/null
+++ b/tests/alive-tv/uf-float/vector-convert.srctgt.ll
@@ -0,0 +1,15 @@
+; TEST-ARGS: --uf-float
+
+define float @src(float noundef %x) {
+  %a = fptosi float %x to i32
+  %res = sitofp i32 %a to float
+  ret float %res
+}
+
+define float @tgt(float noundef %x) {
+  %vec1 = insertelement <4 x float> poison, float %x, i32 0
+  %vec2 = fptosi <4 x float> %vec1 to <4 x i32>
+  %vec3 = sitofp <4 x i32> %vec2 to <4 x float>
+  %res = extractelement <4 x float> %vec3, i32 0
+  ret float %res
+}
\ No newline at end of file
diff --git a/tests/alive-tv/uf-float/vector-unop.srctgt.ll b/tests/alive-tv/uf-float/vector-unop.srctgt.ll
new file mode 100644
index 000000000..09e70791d
--- /dev/null
+++ b/tests/alive-tv/uf-float/vector-unop.srctgt.ll
@@ -0,0 +1,13 @@
+; TEST-ARGS: --uf-float
+
+define float @src(float noundef %x) {
+  %res = fneg float %x
+  ret float %res
+}
+
+define float @tgt(float noundef %x) {
+  %vec1 = insertelement <2 x float> poison, float %x, i32 0
+  %vec2 = fneg <2 x float> %vec1
+  %res = extractelement <2 x float> %vec2, i32 0
+  ret float %res
+}
\ No newline at end of file