diff --git a/barretenberg/cpp/src/CMakeLists.txt b/barretenberg/cpp/src/CMakeLists.txt
index a52b8939764e..e50a20398ae5 100644
--- a/barretenberg/cpp/src/CMakeLists.txt
+++ b/barretenberg/cpp/src/CMakeLists.txt
@@ -82,7 +82,6 @@ add_subdirectory(barretenberg/wasi)
 
 
 if(SMT)
-    include_directories(${CMAKE_CURRENT_SOURCE_DIR} $ENV{HOME}/cvc5/tmp-lib/include)
     add_subdirectory(barretenberg/smt_verification)
 endif()
 
diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt b/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt
index b3fe42c39f5b..10c6998530d9 100644
--- a/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt
+++ b/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt
@@ -1,2 +1,14 @@
-#barretenberg_module(smt_verification common ${CMAKE_SOURCE_DIR}/src/cvc5/tmp-lib/lib/libcvc5.so.1)
-barretenberg_module(smt_verification common proof_system stdlib_primitives $ENV{HOME}/cvc5/tmp-lib/lib/libcvc5.so.1)
\ No newline at end of file
+barretenberg_module(smt_verification common proof_system stdlib_primitives stdlib_sha256 cvc5)
+
+set(CVC5_INCLUDE $ENV{HOME}/cvc5/tmp-lib/include)
+set(CVC5_LIB $ENV{HOME}/cvc5/tmp-lib/lib)
+
+target_include_directories(smt_verification              PUBLIC ${CVC5_INCLUDE})
+target_include_directories(smt_verification_objects      PUBLIC ${CVC5_INCLUDE})
+target_include_directories(smt_verification_tests        PUBLIC ${CVC5_INCLUDE})
+target_include_directories(smt_verification_test_objects PUBLIC ${CVC5_INCLUDE})
+
+target_link_directories(smt_verification                 PUBLIC ${CVC5_LIB})
+target_link_directories(smt_verification_objects         PUBLIC ${CVC5_LIB})
+target_link_directories(smt_verification_tests           PUBLIC ${CVC5_LIB})
+target_link_directories(smt_verification_test_objects    PUBLIC ${CVC5_LIB})
\ No newline at end of file
diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/README.md b/barretenberg/cpp/src/barretenberg/smt_verification/README.md
index 8dfe2fc15486..5fd904c16bbe 100644
--- a/barretenberg/cpp/src/barretenberg/smt_verification/README.md
+++ b/barretenberg/cpp/src/barretenberg/smt_verification/README.md
@@ -71,7 +71,7 @@ To store it on the disk just do
     
     `FFTerm` - the symbolic value that simulates finite field elements. 
 
-    `FFTerm` - the symbolic value that simulates integer elements which behave like finite field ones. Useful, when you want to create range constraints or perform operations like XOR.
+    `FFITerm` - the symbolic value that simulates integer elements which behave like finite field ones. Useful, when you want to create range constraints or perform operations like XOR.
     
     `Bool` - simulates the boolean values and mostly will be used only to simulate complex `if` statements if needed.
 	
diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp
index 508f79042cad..1126a896794a 100644
--- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp
+++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp
@@ -1,8 +1,11 @@
 #pragma once
-#include <cvc5/cvc5.h>
 #include <string>
 #include <unordered_map>
 
+#include <cvc5/cvc5.h>
+
+#include "barretenberg/ecc/curves/bn254/fr.hpp"
+
 namespace smt_solver {
 
 /**
diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp
index d2a1a6c2670c..130fa36f5ea9 100644
--- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp
+++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp
@@ -38,56 +38,55 @@ FFITerm::FFITerm(const std::string& t, Solver* slv, bool isconst, uint32_t base)
         slv->s.assertFormula(ge);
         slv->s.assertFormula(lt);
     } else {
-        std::string tmp = slv->s.mkFiniteFieldElem(t, slv->fp, base).getFiniteFieldValue(); // dumb but works
-        if (tmp[0] == '-') {
-            this->term = slv->s.mkTerm(cvc5::Kind::ADD, { slv->s.mkInteger(tmp), this->modulus });
-        } else {
-            this->term = slv->s.mkInteger(tmp);
-        }
-        // this->term = slv->s.mkInteger(tmp); won't work for now since the assertion will definitely fail
+        // TODO(alex): CVC5 doesn't provide integer initialization from hex. Yet.
+        std::string strvalue = slv->s.mkFiniteFieldElem(t, slv->fp, base).getFiniteFieldValue();
+        this->term = slv->s.mkInteger(strvalue);
+        this->mod();
     }
 }
 
+void FFITerm::mod()
+{
+    this->term = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus });
+}
+
 FFITerm FFITerm::operator+(const FFITerm& other) const
 {
     cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::ADD, { this->term, other.term });
-    res = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, this->modulus });
     return { res, this->solver };
 }
 
 void FFITerm::operator+=(const FFITerm& other)
 {
     this->term = this->solver->s.mkTerm(cvc5::Kind::ADD, { this->term, other.term });
-    this->term =
-        this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); // TODO(alex): is it faster?
 }
 
 FFITerm FFITerm::operator-(const FFITerm& other) const
 {
     cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::SUB, { this->term, other.term });
-    res = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, this->modulus });
     return { res, this->solver };
 }
 
 void FFITerm::operator-=(const FFITerm& other)
 {
     this->term = this->solver->s.mkTerm(cvc5::Kind::SUB, { this->term, other.term });
-    this->term =
-        this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); // TODO(alex): is it faster?
+}
+
+FFITerm FFITerm::operator-() const
+{
+    cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::NEG, { this->term });
+    return { res, this->solver };
 }
 
 FFITerm FFITerm::operator*(const FFITerm& other) const
 {
     cvc5::Term res = solver->s.mkTerm(cvc5::Kind::MULT, { this->term, other.term });
-    res = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, this->modulus });
     return { res, this->solver };
 }
 
 void FFITerm::operator*=(const FFITerm& other)
 {
     this->term = this->solver->s.mkTerm(cvc5::Kind::MULT, { this->term, other.term });
-    this->term =
-        this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); // TODO(alex): is it faster?
 }
 
 /**
@@ -102,34 +101,22 @@ void FFITerm::operator*=(const FFITerm& other)
  */
 FFITerm FFITerm::operator/(const FFITerm& other) const
 {
-    cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { other.term, this->solver->s.mkInteger("0") });
-    nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { nz, this->solver->s.mkBoolean(false) });
-    this->solver->s.assertFormula(nz);
-
-    cvc5::Term res = this->solver->s.mkConst(this->solver->s.getIntegerSort(),
-                                             "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" +
-                                                 std::string(*this) + "_" + std::string(other));
-    cvc5::Term div = this->solver->s.mkTerm(cvc5::Kind::MULT, { res, other.term });
-    div = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { div, this->modulus });
-    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, div });
-    this->solver->s.assertFormula(eq);
-    return { res, this->solver };
+    other != bb::fr(0);
+    FFITerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast<std::string>(*this) + "_" +
+                          static_cast<std::string>(other),
+                      this->solver);
+    res* other == *this;
+    return res;
 }
 
 void FFITerm::operator/=(const FFITerm& other)
 {
-    cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { other.term, this->solver->s.mkInteger("0") });
-    nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { nz, this->solver->s.mkBoolean(false) });
-    this->solver->s.assertFormula(nz);
-
-    cvc5::Term res = this->solver->s.mkConst(this->solver->fp,
-                                             "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" +
-                                                 std::string(*this) + "__" + std::string(other));
-    cvc5::Term div = this->solver->s.mkTerm(cvc5::Kind::MULT, { res, other.term });
-    div = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { div, this->modulus });
-    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, div });
-    this->solver->s.assertFormula(eq);
-    this->term = res;
+    other != bb::fr(0);
+    FFITerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast<std::string>(*this) + "_" +
+                          static_cast<std::string>(other),
+                      this->solver);
+    res* other == *this;
+    this->term = res.term;
 }
 
 /**
@@ -138,7 +125,15 @@ void FFITerm::operator/=(const FFITerm& other)
  */
 void FFITerm::operator==(const FFITerm& other) const
 {
-    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term });
+    FFITerm tmp1 = *this;
+    if (tmp1.term.getNumChildren() > 1) {
+        tmp1.mod();
+    }
+    FFITerm tmp2 = other;
+    if (tmp2.term.getNumChildren() > 1) {
+        tmp2.mod();
+    }
+    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term });
     this->solver->s.assertFormula(eq);
 }
 
@@ -148,8 +143,83 @@ void FFITerm::operator==(const FFITerm& other) const
  */
 void FFITerm::operator!=(const FFITerm& other) const
 {
-    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term });
+    FFITerm tmp1 = *this;
+    if (tmp1.term.getNumChildren() > 1) {
+        tmp1.mod();
+    }
+    FFITerm tmp2 = other;
+    if (tmp2.term.getNumChildren() > 1) {
+        tmp2.mod();
+    }
+    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term });
     eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { eq, this->solver->s.mkBoolean(false) });
     this->solver->s.assertFormula(eq);
 }
+
+FFITerm FFITerm::operator^(const FFITerm& other) const
+{
+    cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::XOR, { this->term, other.term });
+    return { res, this->solver };
+}
+
+void FFITerm::operator^=(const FFITerm& other)
+{
+    this->term = this->solver->s.mkTerm(cvc5::Kind::XOR, { this->term, other.term });
+}
+
+FFITerm operator+(const bb::fr& lhs, const FFITerm& rhs)
+{
+    return rhs + lhs;
+}
+
+FFITerm operator-(const bb::fr& lhs, const FFITerm& rhs)
+{
+    return (-rhs) + lhs;
+}
+
+FFITerm operator*(const bb::fr& lhs, const FFITerm& rhs)
+{
+    return rhs * lhs;
+}
+
+FFITerm operator/(const bb::fr& lhs, const FFITerm& rhs)
+{
+    return FFITerm(lhs, rhs.solver) / rhs;
+}
+
+FFITerm operator^(const bb::fr& lhs, const FFITerm& rhs)
+{
+    return rhs ^ lhs;
+}
+void operator==(const bb::fr& lhs, const FFITerm& rhs)
+{
+    rhs == lhs;
+}
+
+void operator!=(const bb::fr& lhs, const FFITerm& rhs)
+{
+    rhs != lhs;
+}
+
+void FFITerm::operator<(const bb::fr& other) const
+{
+    cvc5::Term lt = this->solver->s.mkTerm(cvc5::Kind::LT, { this->term, FFITerm(other, this->solver) });
+    this->solver->s.assertFormula(lt);
+}
+void FFITerm::operator<=(const bb::fr& other) const
+{
+    cvc5::Term le = this->solver->s.mkTerm(cvc5::Kind::LEQ, { this->term, FFITerm(other, this->solver) });
+    this->solver->s.assertFormula(le);
+}
+void FFITerm::operator>(const bb::fr& other) const
+{
+    cvc5::Term gt = this->solver->s.mkTerm(cvc5::Kind::GT, { this->term, FFITerm(other, this->solver) });
+    this->solver->s.assertFormula(gt);
+}
+void FFITerm::operator>=(const bb::fr& other) const
+{
+    cvc5::Term ge = this->solver->s.mkTerm(cvc5::Kind::GEQ, { this->term, FFITerm(other, this->solver) });
+    this->solver->s.assertFormula(ge);
+}
+
 } // namespace smt_terms
diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp
index 6bb1239557be..3bc465f3e531 100644
--- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp
+++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp
@@ -11,7 +11,6 @@ using namespace smt_solver;
  * Both of them support basic arithmetic operations: +, -, *, /.
  * Check the satisfability of a system and get it's model.
  *
- * @todo TODO(alex): mayb.. Have to patch cvc5 to create integers from hex...
  */
 class FFITerm {
   public:
@@ -19,24 +18,38 @@ class FFITerm {
     cvc5::Term term;
     cvc5::Term modulus;
 
+    static bool isFiniteField() { return false; };
+    static bool isInteger() { return true; };
+
     FFITerm()
         : solver(nullptr)
         , term(cvc5::Term())
         , modulus(cvc5::Term()){};
 
-    explicit FFITerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16);
     FFITerm(cvc5::Term& term, Solver* s)
         : solver(s)
         , term(term)
         , modulus(s->s.mkInteger(s->modulus))
     {}
 
+    explicit FFITerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16);
+
     FFITerm(const FFITerm& other) = default;
     FFITerm(FFITerm&& other) = default;
 
     static FFITerm Var(const std::string& name, Solver* slv);
     static FFITerm Const(const std::string& val, Solver* slv, uint32_t base = 16);
 
+    explicit FFITerm(bb::fr value, Solver* s)
+    {
+        std::stringstream buf; // TODO(#893)
+        buf << value;
+        std::string tmp = buf.str();
+        tmp[1] = '0'; // avoiding `x` in 0x prefix
+
+        *this = Const(tmp, s);
+    }
+
     FFITerm& operator=(const FFITerm& right) = default;
     FFITerm& operator=(FFITerm&& right) = default;
 
@@ -44,6 +57,8 @@ class FFITerm {
     void operator+=(const FFITerm& other);
     FFITerm operator-(const FFITerm& other) const;
     void operator-=(const FFITerm& other);
+    FFITerm operator-() const;
+
     FFITerm operator*(const FFITerm& other) const;
     void operator*=(const FFITerm& other);
     FFITerm operator/(const FFITerm& other) const;
@@ -52,11 +67,20 @@ class FFITerm {
     void operator==(const FFITerm& other) const;
     void operator!=(const FFITerm& other) const;
 
+    FFITerm operator^(const FFITerm& other) const;
+    void operator^=(const FFITerm& other);
+
+    void mod();
+
     operator std::string() const { return term.isIntegerValue() ? term.getIntegerValue() : term.toString(); };
     operator cvc5::Term() const { return term; };
 
     ~FFITerm() = default;
-    friend std::ostream& operator<<(std::ostream& out, const FFITerm& k) { return out << k.term; }
+
+    friend std::ostream& operator<<(std::ostream& out, const FFITerm& term)
+    {
+        return out << static_cast<std::string>(term);
+    }
 
     friend FFITerm batch_add(const std::vector<FFITerm>& children)
     {
@@ -75,6 +99,34 @@ class FFITerm {
         res = slv->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, children[0].modulus });
         return { res, slv };
     }
+
+    // arithmetic compatibility with Fr
+
+    FFITerm operator+(const bb::fr& other) const { return *this + FFITerm(other, this->solver); }
+    void operator+=(const bb::fr& other) { *this += FFITerm(other, this->solver); }
+    FFITerm operator-(const bb::fr& other) const { return *this - FFITerm(other, this->solver); }
+    void operator-=(const bb::fr& other) { *this -= FFITerm(other, this->solver); }
+    FFITerm operator*(const bb::fr& other) const { return *this * FFITerm(other, this->solver); }
+    void operator*=(const bb::fr& other) { *this *= FFITerm(other, this->solver); }
+    FFITerm operator/(const bb::fr& other) const { return *this / FFITerm(other, this->solver); }
+    void operator/=(const bb::fr& other) { *this /= FFITerm(other, this->solver); }
+
+    void operator==(const bb::fr& other) const { *this == FFITerm(other, this->solver); }
+    void operator!=(const bb::fr& other) const { *this != FFITerm(other, this->solver); }
+    FFITerm operator^(const bb::fr& other) const { return *this ^ FFITerm(other, this->solver); }
+    void operator^=(const bb::fr& other) { *this ^= FFITerm(other, this->solver); }
+    void operator<(const bb::fr& other) const;
+    void operator<=(const bb::fr& other) const;
+    void operator>(const bb::fr& other) const;
+    void operator>=(const bb::fr& other) const;
 };
 
+FFITerm operator+(const bb::fr& lhs, const FFITerm& rhs);
+FFITerm operator-(const bb::fr& lhs, const FFITerm& rhs);
+FFITerm operator*(const bb::fr& lhs, const FFITerm& rhs);
+FFITerm operator^(const bb::fr& lhs, const FFITerm& rhs);
+FFITerm operator/(const bb::fr& lhs, const FFITerm& rhs);
+void operator==(const bb::fr& lhs, const FFITerm& rhs);
+void operator!=(const bb::fr& lhs, const FFITerm& rhs);
+
 } // namespace smt_terms
diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp
new file mode 100644
index 000000000000..7fc5e3edbf35
--- /dev/null
+++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp
@@ -0,0 +1,95 @@
+#include <unordered_map>
+
+#include "ffiterm.hpp"
+
+#include <gtest/gtest.h>
+
+namespace {
+auto& engine = bb::numeric::get_debug_randomness();
+}
+
+using namespace smt_terms;
+
+TEST(FFITerm, addition)
+{
+    bb::fr a = bb::fr::random_element();
+    bb::fr b = bb::fr::random_element();
+    bb::fr c = a + b;
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16);
+
+    FFITerm x = FFITerm::Var("x", &s);
+    FFITerm y = FFITerm::Var("y", &s);
+    FFITerm bval = FFITerm(b, &s);
+    FFITerm z = x + y;
+
+    z == c;
+    x == a;
+    ASSERT_TRUE(s.check());
+
+    std::string yvals = s.s.getValue(y.term).getIntegerValue();
+    std::string bvals = s.s.getValue(bval.term).getIntegerValue();
+    ASSERT_EQ(bvals, yvals);
+}
+
+TEST(FFITerm, subtraction)
+{
+    bb::fr a = bb::fr::random_element();
+    bb::fr b = bb::fr::random_element();
+    bb::fr c = a - b;
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16);
+
+    FFITerm x = FFITerm::Var("x", &s);
+    FFITerm y = FFITerm::Var("y", &s);
+    FFITerm bval = FFITerm(b, &s);
+    FFITerm z = x - y;
+
+    z == c;
+    x == a;
+    ASSERT_TRUE(s.check());
+
+    std::string yvals = s.s.getValue(y.term).getIntegerValue();
+    std::string bvals = s.s.getValue(bval.term).getIntegerValue();
+    ASSERT_EQ(bvals, yvals);
+}
+
+TEST(FFITerm, multiplication)
+{
+    bb::fr a = bb::fr::random_element();
+    bb::fr b = bb::fr::random_element();
+    bb::fr c = a * b;
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16);
+
+    FFITerm x = FFITerm::Var("x", &s);
+    FFITerm y = FFITerm::Var("y", &s);
+    FFITerm bval = FFITerm(b, &s);
+    FFITerm z = x * y;
+
+    z == c;
+    x == a;
+    ASSERT_TRUE(s.check());
+
+    std::string yvals = s.s.getValue(y.term).getIntegerValue();
+    std::string bvals = s.s.getValue(bval.term).getIntegerValue();
+    ASSERT_EQ(bvals, yvals);
+}
+
+TEST(FFITerm, division)
+{
+    bb::fr a = bb::fr::random_element();
+    bb::fr b = bb::fr::random_element();
+    bb::fr c = a / b;
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16);
+
+    FFITerm x = FFITerm::Var("x", &s);
+    FFITerm y = FFITerm::Var("y", &s);
+    FFITerm bval = FFITerm(b, &s);
+    FFITerm z = x / y;
+
+    z == c;
+    x == a;
+    ASSERT_TRUE(s.check());
+
+    std::string yvals = s.s.getValue(y.term).getIntegerValue();
+    std::string bvals = s.s.getValue(bval.term).getIntegerValue();
+    ASSERT_EQ(bvals, yvals);
+}
diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp
index 4b96f68b8da6..2dfc0904afdc 100644
--- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp
+++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp
@@ -55,6 +55,12 @@ FFTerm FFTerm::operator-(const FFTerm& other) const
     return { res, this->solver };
 }
 
+FFTerm FFTerm::operator-() const
+{
+    cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { this->term });
+    return { res, this->solver };
+}
+
 void FFTerm::operator-=(const FFTerm& other)
 {
     cvc5::Term tmp_term = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { other.term });
@@ -84,34 +90,22 @@ void FFTerm::operator*=(const FFTerm& other)
  */
 FFTerm FFTerm::operator/(const FFTerm& other) const
 {
-    cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL,
-                                           { other.term, this->solver->s.mkFiniteFieldElem("0", this->solver->fp) });
-    nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { nz, this->solver->s.mkBoolean(false) });
-    this->solver->s.assertFormula(nz);
-
-    cvc5::Term res = this->solver->s.mkConst(this->solver->fp,
-                                             "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" +
-                                                 std::string(*this) + "_" + std::string(other));
-    cvc5::Term div = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { res, other.term });
-    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, div });
-    this->solver->s.assertFormula(eq);
-    return { res, this->solver };
+    other != bb::fr(0);
+    FFTerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast<std::string>(*this) + "_" +
+                         static_cast<std::string>(other),
+                     this->solver);
+    res* other == *this;
+    return res;
 }
 
 void FFTerm::operator/=(const FFTerm& other)
 {
-    cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL,
-                                           { other.term, this->solver->s.mkFiniteFieldElem("0", this->solver->fp) });
-    nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { nz, this->solver->s.mkBoolean(false) });
-    this->solver->s.assertFormula(nz);
-
-    cvc5::Term res = this->solver->s.mkConst(this->solver->fp,
-                                             "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" +
-                                                 std::string(*this) + "__" + std::string(other));
-    cvc5::Term div = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { res, other.term });
-    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, div });
-    this->solver->s.assertFormula(eq);
-    this->term = res;
+    other != bb::fr(0);
+    FFTerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast<std::string>(*this) + "_" +
+                         static_cast<std::string>(other),
+                     this->solver);
+    res* other == *this;
+    this->term = res.term;
 }
 
 /**
@@ -134,4 +128,40 @@ void FFTerm::operator!=(const FFTerm& other) const
     eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { eq, this->solver->s.mkBoolean(false) });
     this->solver->s.assertFormula(eq);
 }
+
+FFTerm operator+(const bb::fr& lhs, const FFTerm& rhs)
+{
+    return rhs + lhs;
+}
+
+FFTerm operator-(const bb::fr& lhs, const FFTerm& rhs)
+{
+    return (-rhs) + lhs;
+}
+
+FFTerm operator*(const bb::fr& lhs, const FFTerm& rhs)
+{
+    return rhs * lhs;
+}
+
+FFTerm operator^(__attribute__((unused)) const bb::fr& lhs, __attribute__((unused)) const FFTerm& rhs)
+{
+    info("Not compatible with Finite Field");
+    return {};
+}
+
+FFTerm operator/(const bb::fr& lhs, const FFTerm& rhs)
+{
+    return FFTerm(lhs, rhs.solver) / rhs;
+}
+
+void operator==(const bb::fr& lhs, const FFTerm& rhs)
+{
+    rhs == lhs;
+}
+
+void operator!=(const bb::fr& lhs, const FFTerm& rhs)
+{
+    rhs != lhs;
+}
 } // namespace smt_terms
\ No newline at end of file
diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp
index 581b185bcb33..e847daea07fb 100644
--- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp
+++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp
@@ -17,20 +17,35 @@ class FFTerm {
     Solver* solver;
     cvc5::Term term;
 
+    static bool isFiniteField() { return true; };
+    static bool isInteger() { return false; };
+
     FFTerm()
         : solver(nullptr)
         , term(cvc5::Term()){};
 
-    explicit FFTerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16);
     FFTerm(cvc5::Term& term, Solver* s)
         : solver(s)
         , term(term){};
+
+    explicit FFTerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16);
+
     FFTerm(const FFTerm& other) = default;
     FFTerm(FFTerm&& other) = default;
 
     static FFTerm Var(const std::string& name, Solver* slv);
     static FFTerm Const(const std::string& val, Solver* slv, uint32_t base = 16);
 
+    FFTerm(bb::fr value, Solver* s)
+    {
+        std::stringstream buf; // TODO(#893)
+        buf << value;
+        std::string tmp = buf.str();
+        tmp[1] = '0'; // avoiding `x` in 0x prefix
+
+        *this = Const(tmp, s);
+    }
+
     FFTerm& operator=(const FFTerm& right) = default;
     FFTerm& operator=(FFTerm&& right) = default;
 
@@ -38,6 +53,8 @@ class FFTerm {
     void operator+=(const FFTerm& other);
     FFTerm operator-(const FFTerm& other) const;
     void operator-=(const FFTerm& other);
+    FFTerm operator-() const;
+
     FFTerm operator*(const FFTerm& other) const;
     void operator*=(const FFTerm& other);
     FFTerm operator/(const FFTerm& other) const;
@@ -46,11 +63,24 @@ class FFTerm {
     void operator==(const FFTerm& other) const;
     void operator!=(const FFTerm& other) const;
 
+    FFTerm operator^(__attribute__((unused)) const FFTerm& other) const
+    {
+        info("Not compatible with Finite Field");
+        return {};
+    }
+    void operator^=(__attribute__((unused)) const FFTerm& other) { info("Not compatible with Finite Field"); };
+
+    void mod(){};
+
     operator std::string() const { return term.isFiniteFieldValue() ? term.getFiniteFieldValue() : term.toString(); };
     operator cvc5::Term() const { return term; };
 
     ~FFTerm() = default;
-    friend std::ostream& operator<<(std::ostream& out, const FFTerm& k) { return out << k.term; }
+
+    friend std::ostream& operator<<(std::ostream& out, const FFTerm& term)
+    {
+        return out << static_cast<std::string>(term);
+    };
 
     friend FFTerm batch_add(const std::vector<FFTerm>& children)
     {
@@ -67,6 +97,39 @@ class FFTerm {
         cvc5::Term res = slv->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, terms);
         return { res, slv };
     }
+
+    // arithmetic compatibility with Fr
+
+    FFTerm operator+(const bb::fr& rhs) const { return *this + FFTerm(rhs, this->solver); }
+    void operator+=(const bb::fr& other) { *this += FFTerm(other, this->solver); }
+    FFTerm operator-(const bb::fr& other) const { return *this - FFTerm(other, this->solver); }
+    void operator-=(const bb::fr& other) { *this -= FFTerm(other, this->solver); }
+    FFTerm operator*(const bb::fr& other) const { return *this * FFTerm(other, this->solver); }
+    void operator*=(const bb::fr& other) { *this *= FFTerm(other, this->solver); }
+    FFTerm operator/(const bb::fr& other) const { return *this / FFTerm(other, this->solver); }
+    void operator/=(const bb::fr& other) { *this /= FFTerm(other, this->solver); }
+
+    void operator==(const bb::fr& other) const { *this == FFTerm(other, this->solver); }
+    void operator!=(const bb::fr& other) const { *this != FFTerm(other, this->solver); }
+
+    FFTerm operator^(__attribute__((unused)) const bb::fr& other) const
+    {
+        info("Not compatible with Finite Field");
+        return {};
+    }
+    void operator^=(__attribute__((unused)) const bb::fr& other) { info("Not compatible with Finite Field"); }
+    void operator<(__attribute__((unused)) const bb::fr& other) const { info("Not compatible with Finite Field"); }
+    void operator<=(__attribute__((unused)) const bb::fr& other) const { info("Not compatible with Finite Field"); }
+    void operator>(__attribute__((unused)) const bb::fr& other) const { info("Not compatible with Finite Field"); }
+    void operator>=(__attribute__((unused)) const bb::fr& other) const { info("Not compatible with Finite Field"); }
 };
 
+FFTerm operator+(const bb::fr& lhs, const FFTerm& rhs);
+FFTerm operator-(const bb::fr& lhs, const FFTerm& rhs);
+FFTerm operator*(const bb::fr& lhs, const FFTerm& rhs);
+FFTerm operator^(__attribute__((unused)) const bb::fr& lhs, __attribute__((unused)) const FFTerm& rhs);
+FFTerm operator/(const bb::fr& lhs, const FFTerm& rhs);
+void operator==(const bb::fr& lhs, const FFTerm& rhs);
+void operator!=(const bb::fr& lhs, const FFTerm& rhs);
+
 } // namespace smt_terms
\ No newline at end of file
diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp
new file mode 100644
index 000000000000..08c987114b09
--- /dev/null
+++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp
@@ -0,0 +1,95 @@
+#include <unordered_map>
+
+#include "ffterm.hpp"
+
+#include <gtest/gtest.h>
+
+namespace {
+auto& engine = bb::numeric::get_debug_randomness();
+}
+
+using namespace smt_terms;
+
+TEST(FFTerm, addition)
+{
+    bb::fr a = bb::fr::random_element();
+    bb::fr b = bb::fr::random_element();
+    bb::fr c = a + b;
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16);
+
+    FFTerm x = FFTerm::Var("x", &s);
+    FFTerm y = FFTerm::Var("y", &s);
+    FFTerm bval = FFTerm(b, &s);
+    FFTerm z = x + y;
+
+    z == c;
+    x == a;
+    ASSERT_TRUE(s.check());
+
+    std::string yvals = s.s.getValue(y.term).getFiniteFieldValue();
+    std::string bvals = s.s.getValue(bval.term).getFiniteFieldValue();
+    ASSERT_EQ(bvals, yvals);
+}
+
+TEST(FFTerm, subtraction)
+{
+    bb::fr a = bb::fr::random_element();
+    bb::fr b = bb::fr::random_element();
+    bb::fr c = a - b;
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16);
+
+    FFTerm x = FFTerm::Var("x", &s);
+    FFTerm y = FFTerm::Var("y", &s);
+    FFTerm bval = FFTerm(b, &s);
+    FFTerm z = x - y;
+
+    z == c;
+    x == a;
+    ASSERT_TRUE(s.check());
+
+    std::string yvals = s.s.getValue(y.term).getFiniteFieldValue();
+    std::string bvals = s.s.getValue(bval.term).getFiniteFieldValue();
+    ASSERT_EQ(bvals, yvals);
+}
+
+TEST(FFTerm, multiplication)
+{
+    bb::fr a = bb::fr::random_element();
+    bb::fr b = bb::fr::random_element();
+    bb::fr c = a * b;
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16);
+
+    FFTerm x = FFTerm::Var("x", &s);
+    FFTerm y = FFTerm::Var("y", &s);
+    FFTerm bval = FFTerm(b, &s);
+    FFTerm z = x * y;
+
+    z == c;
+    x == a;
+    ASSERT_TRUE(s.check());
+
+    std::string yvals = s.s.getValue(y.term).getFiniteFieldValue();
+    std::string bvals = s.s.getValue(bval.term).getFiniteFieldValue();
+    ASSERT_EQ(bvals, yvals);
+}
+
+TEST(FFTerm, division)
+{
+    bb::fr a = bb::fr::random_element();
+    bb::fr b = bb::fr::random_element();
+    bb::fr c = a / b;
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16);
+
+    FFTerm x = FFTerm::Var("x", &s);
+    FFTerm y = FFTerm::Var("y", &s);
+    FFTerm bval = FFTerm(b, &s);
+    FFTerm z = x / y;
+
+    z == c;
+    x == a;
+    ASSERT_TRUE(s.check());
+
+    std::string yvals = s.s.getValue(y.term).getFiniteFieldValue();
+    std::string bvals = s.s.getValue(bval.term).getFiniteFieldValue();
+    ASSERT_EQ(bvals, yvals);
+}
\ No newline at end of file