diff --git a/NEWS.md b/NEWS.md
index 047130370eb..23fc3af2b25 100644
--- a/NEWS.md
+++ b/NEWS.md
@@ -12,8 +12,18 @@ This file contains a summary of important user-visible changes.
   * `BITVECTOR_USUBO` unsigned subtraction overflow detection
   * `BITVECTOR_SSUBO` signed subtraction overflow detection
   * `BITVECTOR_SDIVO` signed division overflow detection
-
 - Support for Web Assembly compilation using Emscripten.
+- Support for the theory of (prime-order) finite fields:
+  * Sorts are created with
+    * C++: `Solver::makeFiniteFieldSort`
+    * SMT-LIB: `(_ FiniteField P)` for prime order `P`
+  * Constants are created with
+    * C++: `Solver::makeFiniteFieldElem`
+    * SMT-LIB: `(as ffN F)` for integer `N` and field sort `F`
+  * The operators are multiplication, addition and negation
+    * C++: kinds `FF_MUL`, `FF_ADD`, and `FF_NEG`
+    * SMT-LIB: operators `ff.mul`, `ff.add`, and `ff.neg`
+  * The only predicate is equality
 
 **Changes**
 
diff --git a/cmake/deps-utils/CoCoALib-0.99800-trace.patch b/cmake/deps-utils/CoCoALib-0.99800-trace.patch
index 1f29b16ebad..0f1ce69fd13 100644
--- a/cmake/deps-utils/CoCoALib-0.99800-trace.patch
+++ b/cmake/deps-utils/CoCoALib-0.99800-trace.patch
@@ -22,6 +22,28 @@ index 4c4d51e..efe50f7 100644
  
  typedef std::list<GPoly> GPolyList;
  
+diff --git a/src/AlgebraicCore/PolyRing-content.C b/src/AlgebraicCore/PolyRing-content.C
+index c5d0a0a..36d6d2b 100644
+--- a/src/AlgebraicCore/PolyRing-content.C
++++ b/src/AlgebraicCore/PolyRing-content.C
+@@ -33,6 +33,7 @@
+ #include "CoCoA/convert.H"
+ #include "CoCoA/error.H"
+ #include "CoCoA/utils.H"  // for len
++#include "CoCoA/TmpGPoly.H"
+ 
+ 
+ #include <vector>
+@@ -128,7 +129,9 @@ namespace CoCoA
+   {
+     const PolyRing Rx = owner(f);
+     RingElem ans(Rx);
++    if (handlersEnabled) reductionStartHandler(f);
+     Rx->myMonic(raw(ans), raw(f));
++    if (handlersEnabled) reductionEndHandler(ans);
+     return ans;
+   }
+ 
 diff --git a/src/AlgebraicCore/SparsePolyOps-reduce.C b/src/AlgebraicCore/SparsePolyOps-reduce.C
 index b5b8b43..11687f0 100644
 --- a/src/AlgebraicCore/SparsePolyOps-reduce.C
diff --git a/examples/api/cpp/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt
index 4a1fac9c2c2..6a6a9d845a7 100644
--- a/examples/api/cpp/CMakeLists.txt
+++ b/examples/api/cpp/CMakeLists.txt
@@ -35,6 +35,10 @@ foreach(example ${CVC5_EXAMPLES_API})
   cvc5_add_example(${example} "" "api/cpp")
 endforeach()
 
+if(USE_COCOA)
+  cvc5_add_example(finite_field "" "api/cpp")
+endif()
+
 set(SYGUS_EXAMPLES_API
   sygus-fun
   sygus-grammar
diff --git a/examples/api/cpp/finite_field.cpp b/examples/api/cpp/finite_field.cpp
new file mode 100644
index 00000000000..02871560419
--- /dev/null
+++ b/examples/api/cpp/finite_field.cpp
@@ -0,0 +1,67 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Alex Ozdemir
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * An example of solving finite field problems with cvc5's cpp API
+ */
+
+#include <cvc5/cvc5.h>
+
+#include <cassert>
+#include <iostream>
+
+using namespace std;
+using namespace cvc5;
+
+int main()
+{
+  Solver solver;
+  solver.setOption("produce-models", "true");
+
+  Sort f5 = solver.mkFiniteFieldSort("5");
+  Term a = solver.mkConst(f5, "a");
+  Term b = solver.mkConst(f5, "b");
+  Term z = solver.mkFiniteFieldElem("0", f5);
+
+  Term inv =
+      solver.mkTerm(EQUAL,
+                    {solver.mkTerm(FINITE_FIELD_ADD,
+                                   {solver.mkTerm(FINITE_FIELD_MULT, {a, b}),
+                                    solver.mkFiniteFieldElem("-1", f5)}),
+                     z});
+  Term aIsTwo = solver.mkTerm(
+      EQUAL,
+      {solver.mkTerm(FINITE_FIELD_ADD, {a, solver.mkFiniteFieldElem("-2", f5)}),
+       z});
+  // ab - 1 = 0
+  solver.assertFormula(inv);
+  // a = 2
+  solver.assertFormula(aIsTwo);
+
+  // should be SAT, with b = 2^(-1)
+  Result r = solver.checkSat();
+  assert(r.isSat());
+
+  cout << "a = " << solver.getValue(a) << endl;
+  cout << "b = " << solver.getValue(b) << endl;
+
+  // b = 2
+  Term bIsTwo = solver.mkTerm(
+      EQUAL,
+      {solver.mkTerm(FINITE_FIELD_ADD, {b, solver.mkFiniteFieldElem("-2", f5)}),
+       z});
+
+  // should be UNSAT, 2*2 - 1 != 0
+  solver.assertFormula(bIsTwo);
+
+  r = solver.checkSat();
+  assert(!r.isSat());
+}
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index 9c80ecb9379..aba0be0a7b0 100644
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -37,7 +37,7 @@ set(EXAMPLES_API_JAVA
    UnsatCores
 )
 
-foreach(example ${EXAMPLES_API_JAVA})
+function(add_java_example example)
   add_jar(${example} ${example}.java
           INCLUDE_JARS "${CVC5_JAR}"
           OUTPUT_DIR "${CMAKE_BINARY_DIR}/bin/api/java")
@@ -53,4 +53,12 @@ foreach(example ${EXAMPLES_API_JAVA})
         ${example}
   )
   set_tests_properties(${EXAMPLE_TEST_NAME} PROPERTIES SKIP_RETURN_CODE 77)
+endfunction()
+
+foreach(example ${EXAMPLES_API_JAVA})
+  add_java_example(${example})
 endforeach()
+
+if(USE_COCOA)
+  add_java_example(FiniteField)
+endif()
diff --git a/examples/api/java/FiniteField.java b/examples/api/java/FiniteField.java
new file mode 100644
index 00000000000..94b7bf36f1c
--- /dev/null
+++ b/examples/api/java/FiniteField.java
@@ -0,0 +1,70 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Alex Ozdemir, Mudathir Mohamed, Liana Hadarean, Morgan Deters
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * An example of solving finite field problems with cvc5's Java API
+ *
+ */
+
+import io.github.cvc5.*;
+import java.util.*;
+
+public class FiniteField
+{
+  public static void main(String args[]) throws CVC5ApiException
+  {
+    Solver slv = new Solver();
+    {
+      slv.setLogic("QF_FF"); // Set the logic
+
+      Sort f5 = slv.mkFiniteFieldSort("5");
+      Term a = slv.mkConst(f5, "a");
+      Term b = slv.mkConst(f5, "b");
+      Term z = slv.mkFiniteFieldElem("0", f5);
+
+      System.out.println("is ff: " + f5.isFiniteField());
+      System.out.println("ff size: " + f5.getFiniteFieldSize());
+      System.out.println("is ff value: " + z.isFiniteFieldValue());
+      System.out.println("ff value: " + z.getFiniteFieldValue());
+
+      Term inv =
+        slv.mkTerm(Kind.EQUAL,
+            slv.mkTerm(Kind.FINITE_FIELD_ADD,
+              slv.mkTerm(Kind.FINITE_FIELD_MULT, a, b),
+              slv.mkFiniteFieldElem("-1", f5)),
+            z);
+
+      Term aIsTwo =
+        slv.mkTerm(Kind.EQUAL,
+            slv.mkTerm(Kind.FINITE_FIELD_ADD,
+              a,
+              slv.mkFiniteFieldElem("-2", f5)),
+            z);
+
+      slv.assertFormula(inv);
+      slv.assertFormula(aIsTwo);
+
+      Result r = slv.checkSat();
+      System.out.println("is sat: " + r.isSat());
+
+      Term bIsTwo =
+        slv.mkTerm(Kind.EQUAL,
+            slv.mkTerm(Kind.FINITE_FIELD_ADD,
+              b,
+              slv.mkFiniteFieldElem("-2", f5)),
+            z);
+
+      slv.assertFormula(bIsTwo);
+      r = slv.checkSat();
+      System.out.println("is sat: " + r.isSat());
+    }
+  }
+}
diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
index c48aa500f9f..f83f4ac0cee 100644
--- a/examples/api/python/CMakeLists.txt
+++ b/examples/api/python/CMakeLists.txt
@@ -48,7 +48,7 @@ execute_process(COMMAND
                 OUTPUT_VARIABLE PYTHON_MODULE_PATH
                 OUTPUT_STRIP_TRAILING_WHITESPACE)
 
-foreach(example ${EXAMPLES_API_PYTHON})
+function(create_python_example example)
   set(example_test example/api/python/${example})
   add_test(
     NAME ${example_test}
@@ -58,4 +58,12 @@ foreach(example ${EXAMPLES_API_PYTHON})
   set_tests_properties(${example_test} PROPERTIES
     LABELS "example"
     ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH}:${CMAKE_SOURCE_DIR}/api/python)
+endfunction()
+
+foreach(example ${EXAMPLES_API_PYTHON})
+  create_python_example(${example})
 endforeach()
+
+if(USE_COCOA)
+  create_python_example("finite_field")
+endif()
diff --git a/examples/api/python/finite_field.py b/examples/api/python/finite_field.py
new file mode 100644
index 00000000000..3f24c28fd3b
--- /dev/null
+++ b/examples/api/python/finite_field.py
@@ -0,0 +1,59 @@
+###############################################################################
+# Top contributors (to current version):
+#   Andrew Reynolds, Alex Ozdemir
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# A simple test for cvc5's finite field solver.
+#
+##
+
+import cvc5
+from cvc5 import Kind
+
+if __name__ == "__main__":
+    slv = cvc5.Solver()
+    slv.setOption("produce-models", "true")
+    F = slv.mkFiniteFieldSort("5")
+    a = slv.mkConst(F, "a")
+    b = slv.mkConst(F, "b")
+
+    inv = slv.mkTerm(
+        Kind.EQUAL,
+        slv.mkTerm(Kind.FINITE_FIELD_MULT, a, b),
+        slv.mkFiniteFieldElem("1", F),
+    )
+    aIsTwo = slv.mkTerm(
+        Kind.EQUAL,
+        a,
+        slv.mkFiniteFieldElem("2", F),
+    )
+    # ab - 1 = 0
+    slv.assertFormula(inv)
+    # a = 2
+    slv.assertFormula(aIsTwo)
+    r = slv.checkSat()
+
+    # should be SAT, with b = 2^(-1)
+    assert r.isSat()
+    print(slv.getValue(a).toPythonObj())
+    assert slv.getValue(b).toPythonObj() == -2
+
+    bIsTwo = slv.mkTerm(
+        Kind.EQUAL,
+        b,
+        slv.mkFiniteFieldElem("2", F),
+    )
+
+    # b = 2
+    slv.assertFormula(bIsTwo)
+    r = slv.checkSat()
+
+    # should be UNSAT, since 2*2 - 1 != 0
+    assert not r.isSat()
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index b34ced5b61b..ef6e2d05a5d 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -73,6 +73,7 @@
 #include "theory/theory_model.h"
 #include "util/bitvector.h"
 #include "util/divisible.h"
+#include "util/finite_field_value.h"
 #include "util/floatingpoint.h"
 #include "util/iand.h"
 #include "util/random.h"
@@ -227,6 +228,11 @@ const static std::unordered_map<Kind, std::pair<internal::Kind, std::string>>
                   internal::Kind::BITVECTOR_ROTATE_RIGHT),
         KIND_ENUM(INT_TO_BITVECTOR, internal::Kind::INT_TO_BITVECTOR),
         KIND_ENUM(BITVECTOR_TO_NAT, internal::Kind::BITVECTOR_TO_NAT),
+        /* Finite Fields --------------------------------------------------- */
+        KIND_ENUM(CONST_FINITE_FIELD, internal::Kind::CONST_FINITE_FIELD),
+        KIND_ENUM(FINITE_FIELD_MULT, internal::Kind::FINITE_FIELD_MULT),
+        KIND_ENUM(FINITE_FIELD_ADD, internal::Kind::FINITE_FIELD_ADD),
+        KIND_ENUM(FINITE_FIELD_NEG, internal::Kind::FINITE_FIELD_NEG),
         /* FP --------------------------------------------------------------- */
         KIND_ENUM(CONST_FLOATINGPOINT, internal::Kind::CONST_FLOATINGPOINT),
         KIND_ENUM(CONST_ROUNDINGMODE, internal::Kind::CONST_ROUNDINGMODE),
@@ -545,6 +551,11 @@ const static std::unordered_map<internal::Kind,
         {internal::Kind::INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR},
         {internal::Kind::INT_TO_BITVECTOR, INT_TO_BITVECTOR},
         {internal::Kind::BITVECTOR_TO_NAT, BITVECTOR_TO_NAT},
+        /* Finite Fields --------------------------------------------------- */
+        {internal::Kind::CONST_FINITE_FIELD, CONST_FINITE_FIELD},
+        {internal::Kind::FINITE_FIELD_MULT, FINITE_FIELD_MULT},
+        {internal::Kind::FINITE_FIELD_ADD, FINITE_FIELD_ADD},
+        {internal::Kind::FINITE_FIELD_NEG, FINITE_FIELD_NEG},
         /* FP -------------------------------------------------------------- */
         {internal::Kind::CONST_FLOATINGPOINT, CONST_FLOATINGPOINT},
         {internal::Kind::CONST_ROUNDINGMODE, CONST_ROUNDINGMODE},
@@ -1411,6 +1422,15 @@ bool Sort::isArray() const
   CVC5_API_TRY_CATCH_END;
 }
 
+bool Sort::isFiniteField() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isFiniteField();
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 bool Sort::isSet() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -1783,6 +1803,19 @@ uint32_t Sort::getBitVectorSize() const
   CVC5_API_TRY_CATCH_END;
 }
 
+/* Finite field sort --------------------------------------------------- */
+
+std::string Sort::getFiniteFieldSize() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_CHECK(isFiniteField()) << "Not a finite field sort.";
+  //////// all checks before this line
+  return d_type->getFfSize().toString();
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 /* Floating-point sort ------------------------------------------------- */
 
 uint32_t Sort::getFloatingPointExponentSize() const
@@ -3072,6 +3105,28 @@ std::string Term::getBitVectorValue(std::uint32_t base) const
   CVC5_API_TRY_CATCH_END;
 }
 
+bool Term::isFiniteFieldValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_node->getKind() == internal::Kind::CONST_FINITE_FIELD;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+std::string Term::getFiniteFieldValue() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(
+      d_node->getKind() == internal::Kind::CONST_FINITE_FIELD, *d_node)
+      << "Term to be a finite field value when calling getFiniteFieldValue()";
+  //////// all checks before this line
+  return d_node->getConst<internal::FiniteFieldValue>().toSignedInteger().toString();
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 bool Term::isUninterpretedSortValue() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -5465,6 +5520,17 @@ Sort Solver::mkBitVectorSort(uint32_t size) const
   CVC5_API_TRY_CATCH_END;
 }
 
+Sort Solver::mkFiniteFieldSort(const std::string& modulus) const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  internal::Integer m(modulus, 10);
+  CVC5_API_ARG_CHECK_EXPECTED(m.isProbablePrime(), modulus) << "modulus is prime";
+  return Sort(d_nm, d_nm->mkFiniteFieldType(m));
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -5899,6 +5965,20 @@ Term Solver::mkBitVector(uint32_t size,
   CVC5_API_TRY_CATCH_END;
 }
 
+Term Solver::mkFiniteFieldElem(const std::string& value, const Sort& sort) const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_ARG_CHECK_EXPECTED(sort.isFiniteField(), sort)
+      << "a finite field sort";
+  //////// all checks before this line
+  internal::Integer v(value, 10);
+  internal::FiniteFieldValue f(v, sort.d_type->getFfSize());
+
+  return mkValHelper<internal::FiniteFieldValue>(d_nm, f);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 Term Solver::mkConstArray(const Sort& sort, const Term& val) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 2d123615c00..264f2a5223d 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -559,6 +559,12 @@ class CVC5_EXPORT Sort
    */
   bool isArray() const;
 
+  /**
+   * Determine if this is a finite field sort.
+   * @return True if the sort is a finite field sort.
+   */
+  bool isFiniteField() const;
+
   /**
    * Determine if this is a Set sort.
    * @return True if the sort is a Set sort.
@@ -792,6 +798,13 @@ class CVC5_EXPORT Sort
    */
   uint32_t getBitVectorSize() const;
 
+  /* Finite field sort --------------------------------------------------- */
+
+  /**
+   * @return The size of the finite field sort.
+   */
+  std::string getFiniteFieldSize() const;
+
   /* Floating-point sort ------------------------------------------------- */
 
   /**
@@ -1531,6 +1544,22 @@ class CVC5_EXPORT Term
    */
   std::string getBitVectorValue(uint32_t base = 2) const;
 
+  /**
+   * @return True if the term is a finite field value.
+   */
+  bool isFiniteFieldValue() const;
+  /**
+   * Get the string representation of a finite field value (base 10).
+   *
+   * @note Asserts isFiniteFieldValue().
+   *
+   * @note Uses the integer representative of smallest absolute value.
+   *
+   * @return The string representation of the integer representation of this
+   * finite field value.
+   */
+  std::string getFiniteFieldValue() const;
+
   /**
    * @return True if the term is an abstract value.
    */
@@ -3301,6 +3330,13 @@ class CVC5_EXPORT Solver
    */
   Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) const;
 
+  /**
+   * Create a finite-field sort.
+   * @param size the modulus of the field. Must be prime.
+   * @return The finite-field sort.
+   */
+  Sort mkFiniteFieldSort(const std::string& size) const;
+
   /**
    * Create a datatype sort.
    * @param dtypedecl The datatype declaration from which the sort is created.
@@ -3674,6 +3710,18 @@ class CVC5_EXPORT Solver
    */
   Term mkBitVector(uint32_t size, const std::string& s, uint32_t base) const;
 
+  /**
+   * Create a finite field constant in a given field from a given string
+   *
+   * @param value The string representation of the constant.
+   * @param sort The field sort
+   *
+   * If size is the field size, the constant needs not be in the range [0,size).
+   * If it is outside this range, it will be reduced modulo size before being
+   * constructed.
+   */
+  Term mkFiniteFieldElem(const std::string& value, const Sort& sort) const;
+
   /**
    * Create a constant array with the provided constant value stored at every
    * index
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 2037b4b0b65..d7e74f89536 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -1940,6 +1940,68 @@ enum Kind : int32_t
    */
   BITVECTOR_TO_NAT,
 
+  /* Finite Fields --------------------------------------------------------- */
+
+  /**
+   * Finite field constant.
+   *
+   * - Create Term of this Kind with:
+   *
+   *   - Solver::mkFiniteFieldElem(const std::string&, const Sort&) const
+   */
+  CONST_FINITE_FIELD,
+  /**
+   * Negation of a finite field element (additive inverse).
+   *
+   * - Arity: ``1``
+   *
+   *   - ``1:`` Term of finite field Sort
+   *
+   * - Create Term of this Kind with:
+   *
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+   */
+  FINITE_FIELD_NEG,
+  /**
+   * Addition of two or more finite field elements.
+   *
+   * - Arity: ``n > 1``
+   *
+   *   - ``1..n:`` Terms of finite field Sort (sorts must match)
+   *
+   * - Create Term of this Kind with:
+   *
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+   */
+  FINITE_FIELD_ADD,
+  /**
+   * Multiplication of two or more finite field elements.
+   *
+   * - Arity: ``n > 1``
+   *
+   *   - ``1..n:`` Terms of finite field Sort (sorts must match)
+   *
+   * - Create Term of this Kind with:
+   *
+   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
+   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+   *
+   * - Create Op of this kind with:
+   *
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+   */
+  FINITE_FIELD_MULT,
+
   /* FP -------------------------------------------------------------------- */
 
   /**
diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java
index 22cba584bec..8075c811c74 100644
--- a/src/api/java/io/github/cvc5/Solver.java
+++ b/src/api/java/io/github/cvc5/Solver.java
@@ -158,6 +158,20 @@ public Sort mkBitVectorSort(int size) throws CVC5ApiException
 
   private native long mkBitVectorSort(long pointer, int size);
 
+  /**
+   * Create a finite field sort.
+   * @param size The size of the finite field sort.
+   * @return The finite field sort.
+   * @throws CVC5ApiException
+   */
+  public Sort mkFiniteFieldSort(String size) throws CVC5ApiException
+  {
+    long sortPointer = mkFiniteFieldSort(pointer, size);
+    return new Sort(sortPointer);
+  }
+
+  private native long mkFiniteFieldSort(long pointer, String size);
+
   /**
    * Create a floating-point sort.
    * @param exp The bit-width of the exponent of the floating-point sort.
@@ -1063,6 +1077,24 @@ public Term mkBitVector(int size, String s, int base) throws CVC5ApiException
 
   private native long mkBitVector(long pointer, int size, String s, int base);
 
+  /**
+   * Create a finite field constant in a given field and for a given value.
+   *
+   * @api.note The given value must fit into a the given finite field.
+   *
+   * @param val The value of the constant.
+   * @param sort The sort of the finite field.
+   * @return The finite field constant.
+   * @throws CVC5ApiException
+   */
+  public Term mkFiniteFieldElem(String val, Sort sort) throws CVC5ApiException
+  {
+    long termPointer = mkFiniteFieldElem(pointer, val, sort.getPointer());
+    return new Term(termPointer);
+  }
+
+  private native long mkFiniteFieldElem(long pointer, String val, long sortPointer);
+
   /**
    * Create a constant array with the provided constant value stored at
    * every index
diff --git a/src/api/java/io/github/cvc5/Sort.java b/src/api/java/io/github/cvc5/Sort.java
index fa5d04d64d4..1ae96a7d1d0 100644
--- a/src/api/java/io/github/cvc5/Sort.java
+++ b/src/api/java/io/github/cvc5/Sort.java
@@ -192,6 +192,17 @@ public boolean isBitVector()
 
   private native boolean isBitVector(long pointer);
 
+  /**
+   * Determine if this is a finite field sort (SMT-LIB: {@code (_ FiniteField i)}).
+   * @return True if this sort is a finite field sort.
+   */
+  public boolean isFiniteField()
+  {
+    return isFiniteField(pointer);
+  }
+
+  private native boolean isFiniteField(long pointer);
+
   /**
    * Determine if this is a floatingpoint sort
    * (SMT-LIB: {@code (_ FloatingPoint eb sb)}).
@@ -710,6 +721,18 @@ public int getBitVectorSize()
 
   private native int getBitVectorSize(long pointer);
 
+  /* Finite field sort --------------------------------------------------- */
+
+  /**
+   * @return The bit-width of the bit-vector sort.
+   */
+  public String getFiniteFieldSize()
+  {
+    return getFiniteFieldSize(pointer);
+  }
+
+  private native String getFiniteFieldSize(long pointer);
+
   /* Floating-point sort ------------------------------------------------- */
 
   /**
diff --git a/src/api/java/io/github/cvc5/Term.java b/src/api/java/io/github/cvc5/Term.java
index eaa0b4505d0..4ec586dfd07 100644
--- a/src/api/java/io/github/cvc5/Term.java
+++ b/src/api/java/io/github/cvc5/Term.java
@@ -518,6 +518,30 @@ public String getBitVectorValue(int base) throws CVC5ApiException
 
   private native String getBitVectorValue(long pointer, int base);
 
+  /**
+   * @return True if the term is a finite field value.
+   */
+  public boolean isFiniteFieldValue()
+  {
+    return isFiniteFieldValue(pointer);
+  }
+
+  private native boolean isFiniteFieldValue(long pointer);
+
+  /**
+   * Get the string representation of a finite field value.
+   *
+   * @api.note Asserts {@code Term#isFiniteFieldValue()}.
+   *
+   * @return The string representation of a finite field value.
+   */
+  public String getFiniteFieldValue() throws CVC5ApiException
+  {
+    return getFiniteFieldValue(pointer);
+  }
+
+  private native String getFiniteFieldValue(long pointer);
+
   /**
    * @return True if the term is an uninterpreted sort value.
    */
diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index 78ef5ee1d54..04ddbc296de 100644
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -179,6 +179,24 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkBitVectorSort(
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
+/*
+ * Class:     io_github_cvc5_Solver
+ * Method:    mkFiniteFieldSort
+ * Signature: (JLjava/lang/String)J
+ */
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkFiniteFieldSort(
+    JNIEnv* env, jobject, jlong pointer, jstring size)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Solver* solver = reinterpret_cast<Solver*>(pointer);
+  const char* cSize = env->GetStringUTFChars(size, nullptr);
+  Sort* sortPointer = new Sort(solver->mkFiniteFieldSort(std::string(cSize)));
+  env->ReleaseStringUTFChars(size, cSize);
+  return reinterpret_cast<jlong>(sortPointer);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+
 /*
  * Class:     io_github_cvc5_Solver
  * Method:    mkFloatingPointSort
@@ -1211,6 +1229,26 @@ Java_io_github_cvc5_Solver_mkBitVector__JILjava_lang_String_2I(
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
+/*
+ * Class:     io_github_cvc5_Solver
+ * Method:    mkFiniteFieldElem
+ * Signature: (JLjava/lang/String;J)J
+ */
+JNIEXPORT jlong JNICALL
+Java_io_github_cvc5_Solver_mkFiniteFieldElem(
+    JNIEnv* env, jobject, jlong pointer, jstring jS, jlong sortPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Solver* solver = reinterpret_cast<Solver*>(pointer);
+  Sort* sort = reinterpret_cast<Sort*>(sortPointer);
+  const char* s = env->GetStringUTFChars(jS, nullptr);
+  std::string cS(s);
+  Term* retPointer = new Term(solver->mkFiniteFieldElem(cS, *sort));
+  env->ReleaseStringUTFChars(jS, s);
+  return reinterpret_cast<jlong>(retPointer);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
 /*
  * Class:     io_github_cvc5_Solver
  * Method:    mkConstArray
diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp
index e3ae45fd7d7..d6764407432 100644
--- a/src/api/java/jni/sort.cpp
+++ b/src/api/java/jni/sort.cpp
@@ -236,6 +236,21 @@ JNIEXPORT jboolean JNICALL Java_io_github_cvc5_Sort_isBitVector(JNIEnv* env,
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 }
 
+/*
+ * Class:     io_github_cvc5_Sort
+ * Method:    isFiniteField
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_io_github_cvc5_Sort_isFiniteField(JNIEnv* env,
+                                                                  jobject,
+                                                                  jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Sort* current = reinterpret_cast<Sort*>(pointer);
+  return static_cast<jboolean>(current->isFiniteField());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
 /*
  * Class:     io_github_cvc5_Sort
  * Method:    isFloatingPoint
@@ -930,6 +945,21 @@ JNIEXPORT jint JNICALL Java_io_github_cvc5_Sort_getBitVectorSize(JNIEnv* env,
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
+/*
+ * Class:     io_github_cvc5_Sort
+ * Method:    getFiniteFieldSize
+ * Signature: (J)I
+ */
+JNIEXPORT jstring JNICALL Java_io_github_cvc5_Sort_getFiniteFieldSize(JNIEnv* env,
+                                                                      jobject,
+                                                                      jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Sort* current = reinterpret_cast<Sort*>(pointer);
+  return env->NewStringUTF(current->getFiniteFieldSize().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
 /*
  * Class:     io_github_cvc5_Sort
  * Method:    getFloatingPointExponentSize
diff --git a/src/api/java/jni/term.cpp b/src/api/java/jni/term.cpp
index db957f7f1d2..6dcf5b8041c 100644
--- a/src/api/java/jni/term.cpp
+++ b/src/api/java/jni/term.cpp
@@ -647,6 +647,35 @@ JNIEXPORT jstring JNICALL Java_io_github_cvc5_Term_getBitVectorValue(
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 }
 
+/*
+ * Class:     io_github_cvc5_Term
+ * Method:    isFiniteFieldValue
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL
+Java_io_github_cvc5_Term_isFiniteFieldValue(JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isFiniteFieldValue());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     io_github_cvc5_Term
+ * Method:    getFiniteFieldValue
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_io_github_cvc5_Term_getFiniteFieldValue(
+    JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  std::string ret = current->getFiniteFieldValue();
+  return env->NewStringUTF(ret.c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
 /*
  * Class:     cvc5_Term
  * Class:     io_github_cvc5_Term
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 1b47d949515..95ddf7ca23f 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -213,6 +213,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         Sort mkArraySort(Sort indexSort, Sort elemSort) except +
         Sort mkBitVectorSort(uint32_t size) except +
         Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) except +
+        Sort mkFiniteFieldSort(const string& size) except +
         Sort mkDatatypeSort(DatatypeDecl dtypedecl) except +
         vector[Sort] mkDatatypeSorts(const vector[DatatypeDecl]& dtypedecls) except +
         Sort mkFunctionSort(const vector[Sort]& sorts, Sort codomain) except +
@@ -275,6 +276,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         Term mkBitVector(const string& s) except +
         Term mkBitVector(const string& s, uint32_t base) except +
         Term mkBitVector(uint32_t size, string& s, uint32_t base) except +
+        Term mkFiniteFieldElem(const string& s, Sort sort) except +
         Term mkConstArray(Sort sort, Term val) except +
         Term mkFloatingPointPosInf(uint32_t exp, uint32_t sig) except +
         Term mkFloatingPointNegInf(uint32_t exp, uint32_t sig) except +
@@ -391,6 +393,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         bint isTuple() except +
         bint isRecord() except +
         bint isArray() except +
+        bint isFiniteField() except +
         bint isSet() except +
         bint isBag() except +
         bint isSequence() except +
@@ -420,6 +423,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         Sort getSequenceElementSort() except +
         size_t getUninterpretedSortConstructorArity() except +
         uint32_t getBitVectorSize() except +
+        string getFiniteFieldSize() except +
         uint32_t getFloatingPointExponentSize() except +
         uint32_t getFloatingPointSignificandSize() except +
         size_t getDatatypeArity() except +
@@ -506,6 +510,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         string getRealValue() except +
         bint isBitVectorValue() except +
         string getBitVectorValue(uint32_t base) except +
+        bint isFiniteFieldValue() except +
+        string getFiniteFieldValue() except +
         bint isUninterpretedSortValue() except +
         string getUninterpretedSortValue() except +
         bint isTupleValue() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 21f09aa93df..e6f5c5158e3 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -901,6 +901,16 @@ cdef class Solver:
         sort.csort = self.csolver.mkFloatingPointSort(exp, sig)
         return sort
 
+    def mkFiniteFieldSort(self, size):
+        """
+            Create a finite field sort.
+
+            :param size: The size of the field. Must be a prime-power.
+        """
+        cdef Sort sort = Sort(self)
+        sort.csort = self.csolver.mkFiniteFieldSort(str(size).encode())
+        return sort
+
     def mkDatatypeSort(self, DatatypeDecl dtypedecl):
         """
             Create a datatype sort.
@@ -1437,6 +1447,18 @@ cdef class Solver:
             raise ValueError("Unexpected inputs to mkBitVector")
         return term
 
+    def mkFiniteFieldElem(self, value, Sort sort):
+        """
+            Create finite field value.
+
+            :return: A Term representing a finite field value.
+            :param value: The value of the element's integer representation.
+            :param sort: The field to create the element in.
+        """
+        cdef Term term = Term(self)
+        term.cterm = self.csolver.mkFiniteFieldElem(str(value).encode(), sort.csort)
+        return term
+
     def mkConstArray(self, Sort sort, Term val):
         """
             Create a constant array with the provided constant value stored at
@@ -3104,6 +3126,14 @@ cdef class Sort:
         """
         return self.csort.isArray()
 
+    def isFiniteField(self):
+        """
+            Determine if this is a finite field sort.
+
+            :return: True if the sort is an array sort.
+        """
+        return self.csort.isFiniteField()
+
     def isSet(self):
         """
             Determine if this is a set sort.
@@ -3400,6 +3430,12 @@ cdef class Sort:
         """
         return self.csort.getBitVectorSize()
 
+    def getFiniteFieldSize(self):
+        """
+            :return: The size of the finite field sort.
+        """
+        return int(self.csort.getFiniteFieldSize().decode())
+
     def getFloatingPointExponentSize(self):
         """
             :return: The bit-width of the exponent of the floating-point sort.
@@ -4041,6 +4077,22 @@ cdef class Term:
         """
         return self.cterm.getBitVectorValue(base).decode()
 
+    def isFiniteFieldValue(self):
+        """
+            :return: True iff this term is a finite field value.
+        """
+        return self.cterm.isFiniteFieldValue()
+
+    def getFiniteFieldValue(self):
+        """
+           .. note:: Asserts :py:meth:`isFiniteFieldValue()`.
+
+           .. note:: Uses the integer representative of smallest absolute value.
+
+           :return: The representation of a finite field value as an integer.
+        """
+        return int(self.cterm.getFiniteFieldValue().decode())
+
     def toPythonObj(self):
         """
             Converts a constant value Term to a Python object.
@@ -4051,6 +4103,7 @@ cdef class Term:
             - **Int    :** Returns a Python int
             - **Real   :** Returns a Python Fraction
             - **BV     :** Returns a Python int (treats BV as unsigned)
+            - **FF     :** Returns a Python int (gives the FF integer representative of smallest absolute value)
             - **String :** Returns a Python Unicode string
             - **Array  :** Returns a Python dict mapping indices to values. The constant base is returned as the default value.
 
@@ -4064,6 +4117,8 @@ cdef class Term:
             return self.getRealValue()
         elif self.isBitVectorValue():
             return int(self.getBitVectorValue(), 2)
+        elif self.isFiniteFieldValue():
+            return self.getFiniteFieldValue()
         elif self.isStringValue():
             return self.getStringValue()
         elif self.getSort().isArray():
diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index 069f2a8e46e..bea022764cd 100644
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -31,7 +31,7 @@
 #include "expr/type_checker.h"
 #include "expr/type_properties.h"
 #include "util/bitvector.h"
-#include "util/ff_val.h"
+#include "util/finite_field_value.h"
 #include "util/integer.h"
 #include "util/poly_util.h"
 #include "util/rational.h"
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 7796e3672b8..da69983a7d2 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -26,7 +26,7 @@
 #include "theory/type_enumerator.h"
 #include "util/bitvector.h"
 #include "util/cardinality.h"
-#include "util/ff_val.h"
+#include "util/finite_field_value.h"
 #include "util/integer.h"
 
 using namespace std;
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 6334335a197..87f956a66cd 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -30,6 +30,7 @@
 #include "parser/bounded_token_buffer.h"
 #include "parser/input.h"
 #include "parser/line_buffer.h"
+#include "parser/parser.h"
 #include "parser/parser_exception.h"
 
 namespace cvc5 {
@@ -250,11 +251,7 @@ inline std::string AntlrInput::tokenTextSubstr(pANTLR3_COMMON_TOKEN token,
 }
 
 inline unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token) {
-  unsigned result;
-  std::stringstream ss;
-  ss << tokenText(token);
-  ss >> result;
-  return result;
+  return stringToUnsigned(tokenText(token));
 }
 
 }  // namespace parser
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index a477fd230f5..9a281b91f7c 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -862,5 +862,14 @@ Term ParserState::mkCharConstant(const std::string& s)
   return d_solver->mkString(std::wstring(1, val));
 }
 
+uint32_t stringToUnsigned(const std::string& str)
+{
+  uint32_t result;
+  std::stringstream ss;
+  ss << str;
+  ss >> result;
+  return result;
+}
+
 }  // namespace parser
 }  // namespace cvc5
diff --git a/src/parser/parser.h b/src/parser/parser.h
index fed7b6015ea..4e9cb6379f1 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -606,6 +606,9 @@ class CVC5_EXPORT ParserState
   Term getSymbol(const std::string& var_name, SymbolType type);
 }; /* class Parser */
 
+/** Compute the unsigned integer for a token. */
+uint32_t stringToUnsigned(const std::string& str);
+
 }  // namespace parser
 }  // namespace cvc5
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 261c7229e4a..62b3eac0bcf 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1122,6 +1122,8 @@ simpleSymbolicExprNoKeyword[std::string& s]
     { s = AntlrInput::tokenText($HEX_LITERAL); }
   | BINARY_LITERAL
     { s = AntlrInput::tokenText($BINARY_LITERAL); }
+  | FIELD_LITERAL
+    { s = AntlrInput::tokenText($FIELD_LITERAL); }
   | symbol[s, CHECK_NONE, SYM_VERBATIM]
   | str[s, false]
   | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK
@@ -1601,6 +1603,16 @@ termAtomic[cvc5::Term& atomTerm]
       std::string binStr = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
       atomTerm = SOLVER->mkBitVector(binStr.size(), binStr, 2);
     }
+  | FIELD_LITERAL
+    {
+      Assert(AntlrInput::tokenText($FIELD_LITERAL).find("#f") == 0);
+      size_t mPos = AntlrInput::tokenText($FIELD_LITERAL).find("m");
+      Assert(mPos > 2);
+      std::string ffValStr = AntlrInput::tokenTextSubstr($FIELD_LITERAL, 2, mPos - 2);
+      std::string ffModStr = AntlrInput::tokenTextSubstr($FIELD_LITERAL, mPos + 1);
+      Sort ffSort = SOLVER->mkFiniteFieldSort(ffModStr);
+      atomTerm = SOLVER->mkFiniteFieldElem(ffValStr, ffSort);
+    }
 
   // String constant
   | str[s, true] { atomTerm = SOLVER->mkString(s, true); }
@@ -1796,7 +1808,7 @@ sortSymbol[cvc5::Sort& t]
 @declarations {
   std::string name;
   std::vector<cvc5::Sort> args;
-  std::vector<uint32_t> numerals;
+  std::vector<std::string> numerals;
   bool indexed = false;
 }
   : sortName[name,CHECK_NONE]
@@ -1805,7 +1817,7 @@ sortSymbol[cvc5::Sort& t]
     }
   | LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;})
     symbol[name,CHECK_NONE,SYM_SORT]
-    ( nonemptyNumeralList[numerals]
+    ( nonemptyNumeralStringList[numerals]
       {
         if (!indexed)
         {
@@ -1879,7 +1891,8 @@ symbol[std::string& id,
   ;
 
 /**
- * Matches a nonempty list of numerals.
+ * Matches a nonempty list of unsigned numerals and returns their unsigned
+ * values, capped at 2^32-1.
  * @param numerals the (empty) vector to house the numerals.
  */
 nonemptyNumeralList[std::vector<uint32_t>& numerals]
@@ -1888,6 +1901,16 @@ nonemptyNumeralList[std::vector<uint32_t>& numerals]
     )+
   ;
 
+/**
+ * Matches a nonempty list of numerals.
+ * @param numerals the (empty) vector to house the numerals.
+ */
+nonemptyNumeralStringList[std::vector<std::string>& numeralStrings]
+  : ( INTEGER_LITERAL
+      { numeralStrings.push_back(AntlrInput::tokenText($INTEGER_LITERAL)); }
+    )+
+  ;
+
 /**
  * Parses a datatype definition
  */
@@ -2126,6 +2149,13 @@ BINARY_LITERAL
   : '#b' ('0' | '1')+
   ;
 
+/**
+ * Matches a finite field constant.
+ */
+FIELD_LITERAL
+  : '#f' INTEGER_LITERAL 'm' INTEGER_LITERAL
+  ;
+
 /**
  * Matches a double-quoted string literal. A double-quote inside a string is
  * escaped with "", e.g., "This is a string literal with "" a single, embedded
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index f08b672979e..f3dea3837f2 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -126,6 +126,13 @@ void Smt2State::addBitvectorOperators()
   addIndexedOperator(BITVECTOR_ROTATE_RIGHT, "rotate_right");
 }
 
+void Smt2State::addFiniteFieldOperators()
+{
+  addOperator(cvc5::FINITE_FIELD_ADD, "ff.add");
+  addOperator(cvc5::FINITE_FIELD_MULT, "ff.mul");
+  addOperator(cvc5::FINITE_FIELD_NEG, "ff.neg");
+}
+
 void Smt2State::addDatatypesOperators()
 {
   ParserState::addOperator(APPLY_CONSTRUCTOR);
@@ -780,6 +787,11 @@ Command* Smt2State::setLogic(std::string name, bool fromCommand)
     addFloatingPointOperators();
   }
 
+  if (d_logic.isTheoryEnabled(internal::theory::THEORY_FF))
+  {
+    addFiniteFieldOperators();
+  }
+
   if (d_logic.isTheoryEnabled(internal::theory::THEORY_SEP))
   {
     addSepOperators();
@@ -921,6 +933,18 @@ void Smt2State::parseOpApplyTypeAscription(ParseOp& p, Sort type)
       p.d_expr = getExpressionForNameAndType(p.d_name, type);
       p.d_name = std::string("");
     }
+    if (p.d_name.find("ff") == 0)
+    {
+      std::string rest = p.d_name.substr(2);
+      if (!type.isFiniteField())
+      {
+        std::stringstream ss;
+        ss << "expected finite field sort to ascribe " << p.d_name
+           << " but found sort: " << type;
+        parseError(ss.str());
+      }
+      p.d_expr = d_solver->mkFiniteFieldElem(rest, type);
+    }
     if (p.d_expr.isNull())
     {
       std::stringstream ss;
@@ -1395,7 +1419,7 @@ Sort Smt2State::getParametricSort(const std::string& name,
 }
 
 Sort Smt2State::getIndexedSort(const std::string& name,
-                               const std::vector<uint32_t>& numerals)
+                               const std::vector<std::string>& numerals)
 {
   Sort ret;
   if (name == "BitVec")
@@ -1404,11 +1428,20 @@ Sort Smt2State::getIndexedSort(const std::string& name,
     {
       parseError("Illegal bitvector type.");
     }
-    if (numerals.front() == 0)
+    uint32_t n0 = stringToUnsigned(numerals[0]);
+    if (n0 == 0)
     {
       parseError("Illegal bitvector size: 0");
     }
-    ret = d_solver->mkBitVectorSort(numerals.front());
+    ret = d_solver->mkBitVectorSort(n0);
+  }
+  else if (name == "FiniteField")
+  {
+    if (numerals.size() != 1)
+    {
+      parseError("Illegal finite field type.");
+    }
+    ret = d_solver->mkFiniteFieldSort(numerals.front());
   }
   else if (name == "FloatingPoint")
   {
@@ -1416,15 +1449,17 @@ Sort Smt2State::getIndexedSort(const std::string& name,
     {
       parseError("Illegal floating-point type.");
     }
-    if (!internal::validExponentSize(numerals[0]))
+    uint32_t n0 = stringToUnsigned(numerals[0]);
+    uint32_t n1 = stringToUnsigned(numerals[1]);
+    if (!internal::validExponentSize(n0))
     {
       parseError("Illegal floating-point exponent size");
     }
-    if (!internal::validSignificandSize(numerals[1]))
+    if (!internal::validSignificandSize(n1))
     {
       parseError("Illegal floating-point significand size");
     }
-    ret = d_solver->mkFloatingPointSort(numerals[0], numerals[1]);
+    ret = d_solver->mkFloatingPointSort(n0, n1);
   }
   else
   {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index dfbc5dd86e4..9350ef8704a 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -374,7 +374,7 @@ class Smt2State : public ParserState
    * Returns a (indexed) sort, given a name and numeric indices.
    */
   Sort getIndexedSort(const std::string& name,
-                      const std::vector<uint32_t>& numerals);
+                      const std::vector<std::string>& numerals);
   //------------------------- end processing parse operators
 
   /**
@@ -399,6 +399,8 @@ class Smt2State : public ParserState
 
   void addBitvectorOperators();
 
+  void addFiniteFieldOperators();
+
   void addDatatypesOperators();
 
   void addStringOperators();
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index a03fd8ffbe5..e97bd3ba52c 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -45,6 +45,7 @@
 #include "theory/uf/function_const.h"
 #include "util/bitvector.h"
 #include "util/divisible.h"
+#include "util/finite_field_value.h"
 #include "util/floatingpoint.h"
 #include "util/iand.h"
 #include "util/indexed_root_predicate.h"
@@ -199,6 +200,9 @@ void Smt2Printer::toStream(std::ostream& out,
     case kind::BITVECTOR_TYPE:
       out << "(_ BitVec " << n.getConst<BitVectorSize>().d_size << ")";
       break;
+    case kind::FINITE_FIELD_TYPE:
+      out << "(_ FiniteField " << n.getConst<FfSize>().d_size << ")";
+      break;
     case kind::FLOATINGPOINT_TYPE:
       out << "(_ FloatingPoint "
           << n.getConst<FloatingPointSize>().exponentWidth() << " "
@@ -217,6 +221,12 @@ void Smt2Printer::toStream(std::ostream& out,
       }
       break;
     }
+    case kind::CONST_FINITE_FIELD:
+    {
+      const FiniteFieldValue& ff = n.getConst<FiniteFieldValue>();
+      out << "#f" << ff.getValue() << "m" << ff.getFieldSize();
+      break;
+    }
     case kind::CONST_FLOATINGPOINT:
     {
       out << n.getConst<FloatingPoint>().toString(
@@ -1136,6 +1146,11 @@ std::string Smt2Printer::smtKindString(Kind k)
     case kind::PARTIAL_SELECT_1: return "partial_select_1";
     case kind::EQ_RANGE: return "eqrange";
 
+    // ff theory
+  case kind::FINITE_FIELD_ADD: return "ff.add";
+  case kind::FINITE_FIELD_MULT: return "ff.mul";
+  case kind::FINITE_FIELD_NEG: return "ff.neg";
+
     // bv theory
     case kind::BITVECTOR_CONCAT: return "concat";
     case kind::BITVECTOR_AND: return "bvand";
diff --git a/src/theory/arith/nl/coverings/cocoa_converter.h b/src/theory/arith/nl/coverings/cocoa_converter.h
index d5d93aa51ac..ade7498344a 100644
--- a/src/theory/arith/nl/coverings/cocoa_converter.h
+++ b/src/theory/arith/nl/coverings/cocoa_converter.h
@@ -115,9 +115,6 @@ class CoCoAConverter
   poly::Polynomial convertImpl(const CoCoA::RingElem& p,
                                poly::Integer& denominator) const;
 
-  /** Some global state that CoCoA needs to be around whenever it is used */
-  CoCoA::GlobalManager d_gm;
-
   /**
    * Maps libpoly variables to indets in CoCoA.
    */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 7df55b79a0b..329fea96da9 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -28,6 +28,7 @@
 #include "theory/ext_theory.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "util/cocoa_globals.h"
 
 using namespace std;
 using namespace cvc5::internal::kind;
@@ -52,6 +53,10 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
       d_rewriter(d_opElim),
       d_arithModelCacheSet(false)
 {
+#ifdef CVC5_USE_COCOA
+  // must be initialized before using CoCoA.
+  initCocoaGlobalManager();
+#endif /* CVC5_USE_COCOA */
   // currently a cyclic dependency to TheoryArithPrivate
   d_astate.setParent(d_internal);
   // indicate we are using the theory state object and inference manager
diff --git a/src/theory/ff/core.cpp b/src/theory/ff/core.cpp
index 4ee43a35363..ea2db46c494 100644
--- a/src/theory/ff/core.cpp
+++ b/src/theory/ff/core.cpp
@@ -62,6 +62,11 @@ void IncrementalTracer::setFunctionPointers()
   CoCoA::reductionEndHandler = d_reductionEnd;
 }
 
+void IncrementalTracer::unsetFunctionPointers()
+{
+  CoCoA::handlersEnabled = false;
+}
+
 void IncrementalTracer::addInput(const CoCoA::RingElem& i)
 {
   Trace("ff::core") << "input: " << i << std::endl;
@@ -209,7 +214,19 @@ void IncrementalTracer::reductionEnd(CoCoA::ConstRefRingElem r)
   }
   else
   {
-    Trace("ff::core") << " drop" << std::endl;
+    if (TraceIsOn("ff::core"))
+    {
+      Trace("ff::core") << " drop" << std::endl;
+      if (d_parents.count(rr))
+      {
+        Trace("ff::core") << " parents:";
+        for (const auto& p : d_parents.at(rr))
+        {
+          Trace("ff::core") << ", " << p;
+        }
+        Trace("ff::core") << std::endl;
+      }
+    }
   }
   d_reductionSeq.clear();
 }
diff --git a/src/theory/ff/core.h b/src/theory/ff/core.h
index 08e650f7fc9..9eacfd07271 100644
--- a/src/theory/ff/core.h
+++ b/src/theory/ff/core.h
@@ -36,22 +36,40 @@ namespace cvc5::internal {
 namespace theory {
 namespace ff {
 
-// An incremental dependency graph for CoCoA polynomials in Groebner basis
-// computation.
+/**
+ * An incremental dependency graph for CoCoA polynomials in Groebner basis
+ * computation.
+ */
 class IncrementalTracer
 {
  public:
-  // Empty graph
+  /**
+   * Empty graph
+   */
   IncrementalTracer();
-  // Hook up to CoCoA handlers.
+  /**
+   * Hook up to CoCoA handlers.
+   */
   void setFunctionPointers();
-  // Add an input to the graph
+  /**
+   * Unhook from CoCoA handlers.
+   */
+  void unsetFunctionPointers();
+  /**
+   * Add an input to the graph
+   */
   void addInput(const CoCoA::RingElem& i);
-  // Get the index of inputs responsible for this element.
+  /**
+   * Get the index of inputs responsible for this element.
+   */
   std::vector<size_t> trace(const CoCoA::RingElem& i) const;
-  // Enter a new context
+  /**
+   * Enter a new context
+   */
   void push();
-  // Remove last context. Resets graph to its state before that context.
+  /**
+   * Remove last context. Resets graph to its state before that context.
+   */
   void pop();
 
  private:
diff --git a/src/theory/ff/groebner.cpp b/src/theory/ff/groebner.cpp
index 8bb78552c0c..73dba7b3641 100644
--- a/src/theory/ff/groebner.cpp
+++ b/src/theory/ff/groebner.cpp
@@ -69,6 +69,8 @@ void IncrementalIdeal::pushGenerators(std::vector<CoCoA::RingElem>&& gens)
   d_context->push();
   d_tracer.push();
   std::vector<CoCoA::RingElem> theseGens = d_basis.get();
+  Trace("ff::groebner::push")
+      << "old gen count " << theseGens.size() << std::endl;
   for (auto& g : gens)
   {
     d_gens.emplace_back(std::move(g));
@@ -80,7 +82,9 @@ void IncrementalIdeal::pushGenerators(std::vector<CoCoA::RingElem>&& gens)
   {
     for (const auto& b : theseGens)
     {
-      Trace("ff::groebner::push") << "gens: " << b << std::endl;
+      Trace("ff::groebner::push")
+          << "gens: " << b << " @ " << CoCoA::RingID(CoCoA::owner(b))
+          << std::endl;
     }
   }
   CoCoA::ideal ideal = CoCoA::ideal(theseGens);
@@ -171,7 +175,9 @@ void IncrementalIdeal::ensureSolution()
 {
   if (!d_hasSolution.get().has_value())
   {
+    d_tracer.unsetFunctionPointers();
     std::vector<CoCoA::RingElem> root = commonRoot(CoCoA::ideal(d_basis.get()));
+    d_tracer.setFunctionPointers();
     if (root.empty())
     {
       d_hasSolution.set({false});
diff --git a/src/theory/ff/groebner.h b/src/theory/ff/groebner.h
index 09afa6f3341..abdde1119b1 100644
--- a/src/theory/ff/groebner.h
+++ b/src/theory/ff/groebner.h
@@ -37,71 +37,107 @@ namespace cvc5::internal {
 namespace theory {
 namespace ff {
 
-// Class for constructing a polynomial ideal for an incremental source of
-// generators.
-//
-// Essentially, you can pass a sequence of generators to this class:
-//
-//     p1, p2, p3, p4, p5, p6, p7
-//
-// in chunks. E.g., p1, p2 and then p3, p4, p5, p6, p7. After each chunk, you
-// can:
-//
-// * check if the whole sequence generates a trivial ideal
-//   * if so, get a subset of the generators that cause triviality
-// * if not, check if the variety (common zero set) for the sequence is empty
-// * if not, get a common zero
-//
-// The class support backtracking/popping: you can remove a chunk of generators
-// at any time.
+/**
+ * Class for constructing a polynomial ideal for an incremental source of
+ * generators.
+ *
+ * Essentially, you can pass a sequence of generators to this class:
+ *
+ *     p1, p2, p3, p4, p5, p6, p7
+ *
+ * in chunks. E.g., p1, p2 and then p3, p4, p5, p6, p7. After each chunk, you
+ * can:
+ *
+ * * check if the whole sequence generates a trivial ideal
+ *   * if so, get a subset of the generators that cause triviality
+ * * if not, check if the variety (common zero set) for the sequence is empty
+ * * if not, get a common zero
+ *
+ * The class support backtracking/popping: you can remove a chunk of generators
+ * at any time.
+ */
 class IncrementalIdeal : EnvObj
 {
  public:
   IncrementalIdeal(Env& env, CoCoA::ring polyRing);
-  // Add new generators
+  /**
+   * Add new generators
+   */
   void pushGenerators(std::vector<CoCoA::RingElem>&& gens);
-  // Is the ideal the whole ring?
+  /**
+   * Is the ideal the whole ring?
+   */
   bool idealIsTrivial();
-  // For a trivial ideal, return a (sub)list of generator indices that generate it.
+  /**
+   * For a trivial ideal, return a (sub)list of generator indices that generate it.
+   */
   const std::vector<size_t>& trivialCoreIndices();
-  // For a trivial ideal, return a (sub)list of generators that generate it.
+  /**
+   * For a trivial ideal, return a (sub)list of generators that generate it.
+   */
   std::vector<CoCoA::RingElem> trivialCore();
-  // For a non-trivial idea, check whether there is a base-field variety member.
+  /**
+   * For a non-trivial idea, check whether there is a base-field variety member.
+   */
   bool hasSolution();
-  // For a non-trivial idea with a base-field variety member, get it.
+  /**
+   * For a non-trivial idea with a base-field variety member, get it.
+   */
   const std::vector<CoCoA::RingElem>& solution();
-  // Remove the last batch of generators
+  /**
+   * Remove the last batch of generators
+   */
   void pop();
 
  private:
-  // Run common-root extraction, ensuring a common root is found if one exists.
+  /**
+   * Run common-root extraction, ensuring a common root is found if one exists.
+   */
   void ensureSolution();
 
-  // Used to manage the sequence of generators. A new context is pushed for
-  // each new chunk of generators, and popped when they are removed.
-  //
-  // With this context, other data structures are automatically updated as
-  // generators are added/removed.
+  /**
+   * Used to manage the sequence of generators. A new context is pushed for
+   * each new chunk of generators, and popped when they are removed.
+   *
+   * With this context, other data structures are automatically updated as
+   * generators are added/removed.
+   */
   std::unique_ptr<context::Context> d_context;
 
-  // The ring that generators/the ideal live in
+  /**
+   * The ring that generators/the ideal live in
+   */
   CoCoA::ring d_polyRing;
-  // Used to record steps in the ideal membership calculus.
+  /**
+   * Used to record steps in the ideal membership calculus.
+   */
   IncrementalTracer d_tracer{};
-  // The sequence of generators
+  /**
+   * The sequence of generators
+   */
   context::CDList<CoCoA::RingElem> d_gens;
-  // A GB for the current generators.
+  /**
+   * A GB for the current generators.
+   */
   context::CDO<std::vector<CoCoA::RingElem>> d_basis;
-  // Whether we've already computed a core for ideal triviality.
+  /**
+   * Whether we've already computed a core for ideal triviality.
+   */
   context::CDO<bool> d_hasCore;
-  // What that core is.
+  /**
+   * What that core is.
+   */
   context::CDO<std::vector<size_t>> d_core;
-  // Whether we've search for a common root, and whether we found one.
-  //
-  // Empty if we haven't searched. True if we found one, False if not.
+  /**
+   * Whether we've search for a common root, and whether we found one.
+   *
+   * Empty if we haven't searched. True if we found one, False if not.
+   */
   context::CDO<std::optional<bool>> d_hasSolution;
 
-  // What the common root is.
+  /**
+   * What the common root is.
+   */
   context::CDO<std::vector<CoCoA::RingElem>> d_solution;
 };
 
diff --git a/src/theory/ff/kinds b/src/theory/ff/kinds
index 9f542948c5d..27699c8ac8e 100644
--- a/src/theory/ff/kinds
+++ b/src/theory/ff/kinds
@@ -19,7 +19,7 @@ constant FINITE_FIELD_TYPE \
   struct \
   FfSize \
   "::cvc5::internal::FfSizeHashFunction" \
-  "util/ff_val.h" \
+  "util/finite_field_value.h" \
   "finite field type"
 
 cardinality FINITE_FIELD_TYPE \
@@ -37,10 +37,10 @@ well-founded FINITE_FIELD_TYPE \
 
 constant CONST_FINITE_FIELD \
   class \
-  FfVal \
-  ::cvc5::internal::FfValHashFunction \
-  "util/ff_val.h" \
-  "a finite-field constant; payload is an instance of the cvc5::internal::FfVal class"
+  FiniteFieldValue \
+  ::cvc5::internal::FiniteFieldValueHashFunction \
+  "util/finite_field_value.h" \
+  "a finite-field constant; payload is an instance of the cvc5::internal::FiniteFieldValue class"
 
 ## ffmetic kinds
 operator FINITE_FIELD_MULT 2: "multiplication of two or more field elements"
diff --git a/src/theory/ff/model.cpp b/src/theory/ff/model.cpp
index 0bad73a12e8..fb0d72e057a 100644
--- a/src/theory/ff/model.cpp
+++ b/src/theory/ff/model.cpp
@@ -259,14 +259,14 @@ std::vector<CoCoA::RingElem> commonRoot(const CoCoA::ideal& initialIdeal)
       branchers.push_back(brancher(ideal));
       Trace("ff::model::branch")
           << "brancher: " << branchers.back()->name() << std::endl;
-  if (TraceIsOn("ff::model::branch"))
-  {
-    Trace("ff::model::branch") << "ideal polys: " << std::endl;
-    for (const auto& p : CoCoA::gens(ideal))
-    {
-      Trace("ff::model::branch") << " * " << p << std::endl;
-    }
-  }
+      if (TraceIsOn("ff::model::branch"))
+      {
+        Trace("ff::model::branch") << "ideal polys: " << std::endl;
+        for (const auto& p : CoCoA::gens(ideal))
+        {
+          Trace("ff::model::branch") << " * " << p << std::endl;
+        }
+      }
     }
     // Otherwise, this ideal should have a brancher; get the next branch
     else
diff --git a/src/theory/ff/model.h b/src/theory/ff/model.h
index 31f41491a5f..415e83b2e16 100644
--- a/src/theory/ff/model.h
+++ b/src/theory/ff/model.h
@@ -35,21 +35,31 @@ namespace cvc5::internal {
 namespace theory {
 namespace ff {
 
-// Find a common zero for all poynomials in this ideal.
+/**
+ * Find a common zero for all poynomials in this ideal.
+ */
 std::vector<CoCoA::RingElem> commonRoot(const CoCoA::ideal& ideal);
 
-// Enumerates **assignment**s: monic, degree-one, univariate polynomials.
+/**
+ * Enumerates **assignment**s: monic, degree-one, univariate polynomials.
+ */
 class AssignmentEnumerator
 {
  public:
   virtual ~AssignmentEnumerator();
-  // Return the next assignment, or an empty option.
+  /**
+   * Return the next assignment, or an empty option.
+   */
   virtual std::optional<CoCoA::RingElem> next() = 0;
-  // get the name of this enumerator
+  /**
+   * get the name of this enumerator
+   */
   virtual std::string name() = 0;
 };
 
-// Guess a prescribed set of values for a variable.
+/**
+ * Guess a prescribed set of values for a variable.
+ */
 class ListEnumerator : public AssignmentEnumerator
 {
  public:
@@ -62,27 +72,31 @@ class ListEnumerator : public AssignmentEnumerator
   std::vector<CoCoA::RingElem> d_remainingOptions;
 };
 
-// Return a list enumerator whose elements are (real) factors of this
-// polynomial.
+/**
+ * Return a list enumerator whose elements are (real) factors of this
+ * polynomial.
+ */
 std::unique_ptr<ListEnumerator> factorEnumerator(
     CoCoA::RingElem univariatePoly);
 
-// Guess all values for all variables, in a round robin. Only works for a prime
-// field (order p):
-//
-// * v0: 0
-// * v1: 0
-// * ...
-// * vN: 0
-// * v0: 1
-// * v1: 1
-// * ...
-// * vN: 1
-// * .....
-// * v0: p-1
-// * v1: p-1
-// * ...
-// * vN: p-1
+/**
+ * Guess all values for all variables, in a round robin. Only works for a prime
+ * field (order p):
+ *
+ * * v0: 0
+ * * v1: 0
+ * * ...
+ * * vN: 0
+ * * v0: 1
+ * * v1: 1
+ * * ...
+ * * vN: 1
+ * * .....
+ * * v0: p-1
+ * * v1: p-1
+ * * ...
+ * * vN: p-1
+ */
 class RoundRobinEnumerator : public AssignmentEnumerator
 {
  public:
@@ -99,36 +113,46 @@ class RoundRobinEnumerator : public AssignmentEnumerator
   CoCoA::BigInt d_maxIdx;
 };
 
-// Is this ideal the whole ring?
-//
-// That is, does this ideal contain all polynomials, including all non-zero
-// constant polynomials (which have no zeros).
-//
-// This is a sound, but incomplete test for there being no common zeros (the
-// system being UNSAT).
-//
-// For an example of incompleteness, the ideal generated by just X^2+1 is not
-// the whole ring, but has no zeros in the field of order three.
+/**
+ * Is this ideal the whole ring?
+ *
+ * That is, does this ideal contain all polynomials, including all non-zero
+ * constant polynomials (which have no zeros).
+ *
+ * This is a sound, but incomplete test for there being no common zeros (the
+ * system being UNSAT).
+ *
+ * For an example of incompleteness, the ideal generated by just X^2+1 is not
+ * the whole ring, but has no zeros in the field of order three.
+ */
 bool isUnsat(const CoCoA::ideal& ideal);
 
-// Given a univariate linear polynomial, extract the assignment that satisfies
-// it.
-//
-// An assignment is a variable number and a coefficient ring value.
+/**
+ * Given a univariate linear polynomial, extract the assignment that satisfies
+ * it.
+ *
+ * An assignment is a variable number and a coefficient ring value.
+ */
 std::pair<size_t, CoCoA::RingElem> extractAssignment(
     const CoCoA::RingElem& elem);
 
-// Which variables are assigned? Represented as strings.
+/**
+ * Which variables are assigned? Represented as strings.
+ */
 std::unordered_set<std::string> assignedVars(const CoCoA::ideal& ideal);
 
-// Are all variables assigned?
+/**
+ * Are all variables assigned?
+ */
 bool allVarsAssigned(const CoCoA::ideal& ideal);
 
-// Compute a brancher
-//
-// * based on a univariate, super-linear polynomial if one exists
-// * o.w., a minimal polynomial if the variety is zero-dimensional
-// * o.w., a round-robin guesser.
+/**
+ * Compute a brancher
+ *
+ * * based on a univariate, super-linear polynomial if one exists
+ * * o.w., a minimal polynomial if the variety is zero-dimensional
+ * * o.w., a round-robin guesser.
+ */
 std::unique_ptr<AssignmentEnumerator> brancher(const CoCoA::ideal& ideal);
 
 }  // namespace ff
diff --git a/src/theory/ff/roots.h b/src/theory/ff/roots.h
index dc5fc3a7ecb..1ff2c82acc5 100644
--- a/src/theory/ff/roots.h
+++ b/src/theory/ff/roots.h
@@ -30,15 +30,19 @@ namespace cvc5::internal {
 namespace theory {
 namespace ff {
 
-// Given a univariate f over a finite field, return the monic polynomial with
-// the same base-field roots as f, of minimal degree.
-//
-// Thus, the return is a polynomial with unique linear factors
+/**
+ * Given a univariate f over a finite field, return the monic polynomial with
+ * the same base-field roots as f, of minimal degree.
+ *
+ * Thus, the return is a polynomial with unique linear factors
+ */
 CoCoA::RingElem distinctRootsPoly(CoCoA::RingElem f);
 
-// Given a univariate f over a finite field, return a list of roots in that field.
-//
-// The list is sorted.
+/**
+ * Given a univariate f over a finite field, return a list of roots in that field.
+ *
+ * The list is sorted.
+ */
 std::vector<CoCoA::RingElem> roots(CoCoA::RingElem f);
 
 }  // namespace ff
diff --git a/src/theory/ff/stats.h b/src/theory/ff/stats.h
index 8e48c66dc65..ae29b93c3ae 100644
--- a/src/theory/ff/stats.h
+++ b/src/theory/ff/stats.h
@@ -28,13 +28,21 @@ namespace ff {
 
 struct FfStatistics
 {
-  // Number of groebner-basis reductions
+  /**
+   * Number of groebner-basis reductions
+   */
   IntStat d_numReductions;
-  // Time spent in groebner-basis reductions
+  /**
+   * Time spent in groebner-basis reductions
+   */
   TimerStat d_reductionTime;
-  // Time spent in model construction
+  /**
+   * Time spent in model construction
+   */
   TimerStat d_modelConstructionTime;
-  // Number of times that model construction gave an error
+  /**
+   * Number of times that model construction gave an error
+   */
   IntStat d_numConstructionErrors;
 
   FfStatistics(StatisticsRegistry& reg, const std::string& prefix);
diff --git a/src/theory/ff/sub_theory.cpp b/src/theory/ff/sub_theory.cpp
index 3480a5be158..410eb372bb3 100644
--- a/src/theory/ff/sub_theory.cpp
+++ b/src/theory/ff/sub_theory.cpp
@@ -28,7 +28,7 @@
 #include "options/ff_options.h"
 #include "smt/env_obj.h"
 #include "util/cocoa_globals.h"
-#include "util/ff_val.h"
+#include "util/finite_field_value.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -38,8 +38,7 @@ SubTheory::SubTheory(Env& env, FfStatistics* stats, Integer modulus)
     : EnvObj(env),
       context::ContextNotifyObj(context()),
       d_facts(context()),
-      d_vars(userContext()),
-      d_atoms(userContext()),
+      d_leaves(userContext()),
       d_stats(stats),
       d_baseRing(CoCoA::NewZZmod(CoCoA::BigIntFromString(modulus.toString()))),
       d_modulus(modulus)
@@ -51,14 +50,11 @@ SubTheory::SubTheory(Env& env, FfStatistics* stats, Integer modulus)
 
 void SubTheory::preRegisterTerm(TNode n)
 {
-  if (n.isVar())
+  if (Theory::isLeafOf(n, TheoryId::THEORY_FF) && !n.isConst())
   {
     clearPolyRing();
-    d_vars.push_back(n);
-  }
-  else if (n.getKind() == Kind::EQUAL)
-  {
-    d_atoms.push_back(n);
+    Trace("ff::register") << "FF variable: " << n << std::endl;
+    d_leaves.push_back(n);
   }
 }
 
@@ -96,32 +92,47 @@ void SubTheory::ensureInitPolyRing()
 {
   if (!d_polyRing.has_value())
   {
+    Trace("ff::trans") << "reinitializing CoCoA poly ring" << std::endl;
     std::vector<CoCoA::symbol> symbols;
-    for (const auto& v : d_vars)
+    size_t leaf_num = 0;
+    for (const auto& v : d_leaves)
     {
-      symbols.push_back(CoCoA::symbol(varNameToSymName(v.getName())));
+      std::string name;
+      if (v.isVar())
+      {
+        name = v.getName();
+      }
+      else
+      {
+        name = "leaf" + std::to_string(leaf_num);
+        ++leaf_num;
+      }
+      Trace("ff::trans") << "var " << name << std::endl;
+      symbols.push_back(CoCoA::symbol(varNameToSymName(name)));
     }
-    for (size_t i = 0; i < d_atoms.size(); ++i)
+    for (size_t i = 0; i < d_numInverses; ++i)
     {
       symbols.push_back(CoCoA::symbol("i", i));
     }
     d_polyRing = CoCoA::NewPolyRing(d_baseRing, symbols);
     size_t i = 0;
     Assert(d_translationCache.empty());
-    Assert(d_symbolIdxVars.empty());
-    for (const auto& v : d_vars)
+    Assert(d_symbolIdxLeaves.empty());
+    for (const auto& v : d_leaves)
     {
       d_translationCache.insert({v, CoCoA::indet(d_polyRing.value(), i)});
-      d_symbolIdxVars.insert({i, v});
+      d_symbolIdxLeaves.insert({i, v});
       ++i;
     }
+    Assert(d_inverses.empty());
     Assert(d_atomInverses.empty());
-    for (const auto& a : d_atoms)
+    for (size_t j = 0; j < d_numInverses; ++j)
     {
-      d_atomInverses.insert({a, CoCoA::indet(d_polyRing.value(), i)});
-      Trace("ff::trans") << "inverse for " << a << std::endl;
+      d_inverses.push_back(CoCoA::indet(d_polyRing.value(), i));
       ++i;
     }
+    Trace("ff::trans") << "num allocated inverses: " << d_numInverses
+                       << std::endl;
     Assert(!d_incrementalIdeal.has_value());
     Assert(d_updateIndices.empty());
     d_incrementalIdeal.emplace(d_env, d_polyRing.value());
@@ -134,9 +145,10 @@ void SubTheory::clearPolyRing()
   d_polyRing.reset();
   d_checkIndices.clear();
   d_atomInverses.clear();
+  d_inverses.clear();
   d_translationCache.clear();
   d_incrementalIdeal.reset();
-  d_symbolIdxVars.clear();
+  d_symbolIdxLeaves.clear();
   d_updateIndices.clear();
 }
 
@@ -195,12 +207,20 @@ const std::unordered_map<Node, Node>& SubTheory::model() const
 void SubTheory::contextNotifyPop()
 {
   Trace("ff::context") << "Pop " << context()->getLevel() << std::endl;
-  while (d_updateIndices.back() > d_facts.size())
+  // d_facts is a list of facts received that is sync'd with the external
+  // context.
+  // Now we need to sync up d_updateIndices and d_checkIndices.
+
+  // while d_updateIndices has an OOB ref to d_facts, remove it (and pop the
+  // incremental ideal)
+  while (d_updateIndices.size() > 0 && d_updateIndices.back() > d_facts.size())
   {
     d_updateIndices.pop_back();
     d_incrementalIdeal.value().pop();
     d_conflict.clear();
   }
+
+  // while d_checkIndices has an OOB ref to d_facts, remove it
   while (d_checkIndices.size() > 0 && d_checkIndices.back() > d_facts.size())
   {
     d_checkIndices.pop_back();
@@ -211,31 +231,50 @@ void SubTheory::computeBasis(size_t factIndex)
 {
   Assert(d_conflict.empty());
   Assert(d_updateIndices.size() > 0);
-  Assert(factIndex > d_updateIndices.back());
-  IncrementalIdeal& ideal = d_incrementalIdeal.value();
-  std::vector<CoCoA::RingElem> newGens;
-  for (size_t i = d_updateIndices.back(); i < factIndex; ++i)
+  Assert(factIndex >= d_updateIndices.back());
+  if (factIndex > d_updateIndices.back())
   {
-    TNode fact = d_facts[i];
-    translate(fact);
-    newGens.push_back(d_translationCache.at(fact));
-  }
-  {
-    CodeTimer reductionTimer(d_stats->d_reductionTime);
-    ideal.pushGenerators(std::move(newGens));
-    d_stats->d_numReductions += 1;
-  }
-  d_updateIndices.push_back(factIndex);
-  if (ideal.idealIsTrivial())
-  {
-    for (size_t i : ideal.trivialCoreIndices())
+    // ensure we have enough inverses for all the new disequalities.
+    size_t numDisequalities = 0;
+    for (size_t i = d_updateIndices.back(); i < factIndex; ++i)
     {
-      d_conflict.push_back(d_facts[i]);
+      if (d_facts[i].getKind() == Kind::NOT
+          && d_atomInverses.count(d_facts[i][0]) == 0)
+      {
+        ++numDisequalities;
+      }
     }
-    Trace("ff::conflict") << "conflict " << ideal.trivialCoreIndices().size()
-                          << "/" << d_facts.size() << " facts" << std::endl;
-    if (TraceChannel.isOn("ff::conflict"))
+    ensureInverses(numDisequalities);
+
+    // build the new generators
+    std::vector<CoCoA::RingElem> newGens;
+    for (size_t i = d_updateIndices.back(); i < factIndex; ++i)
     {
+      TNode fact = d_facts[i];
+      translate(fact);
+      newGens.push_back(d_translationCache.at(fact));
+      const auto& b = newGens.back();
+      Trace("ff::groebner::push")
+          << "gens: " << fact << " " << b << " @ "
+          << CoCoA::RingID(CoCoA::owner(b)) << std::endl;
+    }
+
+    // Feed them to the ideal
+    IncrementalIdeal& ideal = d_incrementalIdeal.value();
+    {
+      CodeTimer reductionTimer(d_stats->d_reductionTime);
+      ideal.pushGenerators(std::move(newGens));
+      d_stats->d_numReductions += 1;
+    }
+    d_updateIndices.push_back(factIndex);
+    if (ideal.idealIsTrivial())
+    {
+      for (size_t i : ideal.trivialCoreIndices())
+      {
+        d_conflict.push_back(d_facts[i]);
+      }
+      Trace("ff::conflict") << "conflict " << ideal.trivialCoreIndices().size()
+                            << "/" << d_facts.size() << " facts" << std::endl;
       Trace("ff::conflict::debug")
           << "conflict " << NodeManager::currentNM()->mkAnd(d_conflict)
           << std::endl;
@@ -254,15 +293,15 @@ void SubTheory::extractModel()
     Trace("ff::model") << "found model" << std::endl;
     const auto& values = ideal.solution();
     NodeManager* nm = NodeManager::currentNM();
-    for (size_t i = 0, numVars = d_vars.size(); i < numVars; ++i)
+    for (size_t i = 0, numVars = d_leaves.size(); i < numVars; ++i)
     {
       std::ostringstream symName;
       symName << CoCoA::indet(d_polyRing.value(), i);
-      Node var = d_symbolIdxVars.at(i);
+      Node var = d_symbolIdxLeaves.at(i);
       std::ostringstream valStr;
       valStr << values[i];
       Integer integer(valStr.str(), 10);
-      FfVal literal(integer, d_modulus);
+      FiniteFieldValue literal(integer, d_modulus);
       Node value = nm->mkConst(literal);
 
       Trace("ff::model") << var << ": " << value << std::endl;
@@ -276,15 +315,30 @@ void SubTheory::extractModel()
   }
 }
 
+void SubTheory::ensureInverses(size_t numDisequalities)
+{
+  while (d_atomInverses.size() + numDisequalities >= d_numInverses)
+  {
+    d_numInverses *= 2;
+    Trace("ff::trans") << "Increasing number of inverses to " << d_numInverses
+                       << std::endl;
+    clearPolyRing();
+  }
+  ensureInitPolyRing();
+}
+
 void SubTheory::translate(TNode t)
 {
   auto& cache = d_translationCache;
+  Assert(d_polyRing.has_value());
   // Build polynomials for terms
   for (const auto& node :
        NodeDfsIterable(t, VisitOrder::POSTORDER, [&cache](TNode nn) {
          return cache.count(nn) > 0;
        }))
   {
+    Trace("ff::trans") << "Translating " << node << std::endl;
+    Trace("ff::trans") << "size " << cache.size() << std::endl;
     if (node.getType().isFiniteField() || node.getKind() == Kind::EQUAL
         || node.getKind() == Kind::NOT)
     {
@@ -315,19 +369,37 @@ void SubTheory::translate(TNode t)
         case Kind::CONST_FINITE_FIELD:
           poly = d_polyRing.value()->myOne()
                  * CoCoA::BigIntFromString(
-                     node.getConst<FfVal>().getValue().toString());
+                     node.getConst<FiniteFieldValue>().getValue().toString());
           break;
         // fact cases:
-        case Kind::EQUAL: poly = subPolys[0] - subPolys[1]; break;
+        case Kind::EQUAL:
+          Assert(node[0].getType().isFiniteField());
+          poly = subPolys[0] - subPolys[1];
+          break;
         case Kind::NOT:
+        {
+          auto it = d_atomInverses.find(node[0]);
           Assert(node[0].getKind() == Kind::EQUAL);
-          poly = subPolys[0] * d_atomInverses.at(node[0]) - 1;
+          Assert(node[0][0].getType().isFiniteField());
+          CoCoA::RingElem inverse;
+          if (it == d_atomInverses.end())
+          {
+            // ensure we have a spare inverse
+            Assert(d_atomInverses.size() < d_inverses.size())
+                << "Cannot translate when out of inverses" << std::endl;
+            size_t next = d_atomInverses.size();
+            it = d_atomInverses.insert(it, {node[0], d_inverses[next]});
+          }
+          Assert(it != d_atomInverses.end());
+          inverse = it->second;
+          poly = subPolys[0] * inverse - 1;
           break;
+        }
         default:
           Unreachable() << "Invalid finite field kind: " << node.getKind();
       }
-      Trace("ff::trans")
-          << "Translated " << node << "\t-> " << poly << std::endl;
+      Trace("ff::trans") << "Translated " << node << "\t-> " << poly
+                         << std::endl;
       cache.insert(std::make_pair(node, poly));
     }
   }
diff --git a/src/theory/ff/sub_theory.h b/src/theory/ff/sub_theory.h
index f0f21ef9745..60d487cd9eb 100644
--- a/src/theory/ff/sub_theory.h
+++ b/src/theory/ff/sub_theory.h
@@ -59,108 +59,191 @@ namespace ff {
 class SubTheory : protected EnvObj, protected context::ContextNotifyObj
 {
  public:
-  // Create a new sub-theory.
-  //
-  // Parameters:
-  // * modulus: the size of this field for this theory, a prime.
+  /**
+   * Create a new sub-theory.
+   *
+   * Parameters:
+   * * modulus: the size of this field for this theory, a prime.
+   */
   SubTheory(Env& env, FfStatistics* stats, Integer modulus);
 
-  // Notify this theory of a node it may need to handle.
-  //
-  // All nodes this theory sees in the future must be pre-registered.
+  /**
+   * Notify this theory of a node it may need to handle.
+   *
+   * All nodes this theory sees in the future must be pre-registered.
+   */
   void preRegisterTerm(TNode);
 
-  // Assert a fact to this theory.
+  /**
+   * Assert a fact to this theory.
+   */
   void notifyFact(TNode fact);
 
-  // Check the current facts.
+  /**
+   * Check the current facts.
+   */
   void postCheck(Theory::Effort);
 
-  // Has a conflict been detected?
+  /**
+   * Has a conflict been detected?
+   */
   bool inConflict() const;
 
-  // What is that conflict?
+  /**
+   * What is that conflict?
+   */
   const std::vector<Node>& conflict() const;
 
-  // Get a model.
-  //
-  // Can only be called after a full-effort post-check
-  // if inConflict is false.
+  /**
+   * Get a model.
+   *
+   * Can only be called after a full-effort post-check
+   * if inConflict is false.
+   */
   const std::unordered_map<Node, Node>& model() const;
 
  private:
-  // Called on SAT pop; we pop the incremental ideal if needed.
+  /**
+   * Called on SAT pop; we pop the incremental ideal if needed.
+   */
   void contextNotifyPop() override;
 
-  // Compute a Groebner basis for the facts up to (not including) this index.
+  /**
+   * Compute a Groebner basis for the facts up to (not including) this index.
+   */
   void computeBasis(size_t factIndex);
 
   void extractModel();
 
-  // Initialize the polynomial ring, set up post-registration data structures.
+  /**
+   * Initialize the polynomial ring, set up post-registration data structures.
+   */
   void ensureInitPolyRing();
 
-  // Uninitialize the polynomial ring, clear post-registration data structures.
+  /**
+   * Uninitialize the polynomial ring, clear post-registration data structures.
+   */
   void clearPolyRing();
 
-  // Translate t to CoCoA, and cache the result.
+  /**
+   * Ensure we have at least `numDisequalities` spare inverses.
+   *
+   * If more inverses are added, this will call clearPolyRing.
+   */
+  void ensureInverses(size_t numDisequalities);
+
+  /**
+   * Translate t to CoCoA, and cache the result.
+   *
+   * This will never call clearPolyRing.
+   */
   void translate(TNode t);
 
-  // Is registration done and the polynomial ring initialized?
+  /**
+   * Is registration done and the polynomial ring initialized?
+   */
   bool d_registrationDone();
 
-  // Manages the incremental GB.
+  /**
+   * Manages the incremental GB.
+   */
   std::optional<IncrementalIdeal> d_incrementalIdeal{};
 
-  // For an atom x == y, contains the potential inverse of (x - y).
-  //
-  // Used to make x != y.
+  /**
+   * For an atom x == y, contains the potential inverse of (x - y).
+   *
+   * Used to make x != y.
+   *
+   * Perhaps this could be contextual, to more eagerly free inverses.
+   */
   std::unordered_map<Node, CoCoA::RingElem> d_atomInverses{};
 
-  // Facts, in notification order.
-  //
-  // Contains only the facts in *this specific field*.
-  //
-  // Uses SAT context.
+  /**
+   * An array of inverses. They're used from index 0 upward.
+   */
+  std::vector<CoCoA::RingElem> d_inverses{};
+
+  /**
+   * Facts, in notification order.
+   *
+   * Contains only the facts in *this specific field*.
+   *
+   * Uses SAT context.
+   */
   context::CDList<Node> d_facts;
 
-  // The length of that fact list at each check.
+  /**
+   * The length of that fact list at each check.
+   */
   std::vector<size_t> d_checkIndices{};
 
-  // The length of that fact list at each point where we updated the ideal.
+  /**
+   * The length of that fact list at each point where we updated the ideal.
+   */
   std::vector<size_t> d_updateIndices{};
 
-  // Non-empty if we're in a conflict.
+  /**
+   * Non-empty if we're in a conflict.
+   */
   std::vector<Node> d_conflict{};
 
-  // Cache from nodes to CoCoA polynomials.
+  /**
+   * Cache from nodes to CoCoA polynomials.
+   */
   std::unordered_map<Node, CoCoA::RingElem> d_translationCache{};
 
-  // A model, if we've found one. A map from variable nodes to their constant
-  // values.
+  /**
+   * A model, if we've found one. A map from variable nodes to their constant
+   * values.
+   */
   std::unordered_map<Node, Node> d_model{};
 
-  // Variables
-  context::CDList<Node> d_vars;
-
-  // Variables
-  std::unordered_map<size_t, Node> d_symbolIdxVars{};
-
-  // Atoms
-  context::CDList<Node> d_atoms;
-
-  // Statistics shared among all finite-field sub-theories.
+  /**
+   * Theory leaves
+   */
+  context::CDList<Node> d_leaves;
+
+  /**
+   * Map from CoCoA Indeterminate symbol indexes to leaves
+   */
+  std::unordered_map<size_t, Node> d_symbolIdxLeaves{};
+
+  /**
+   * When asserted, a diseq (not (= a b))
+   * is represented internally to FF as (= (* (- a b) w) 1)
+   * for fresh w, called an "inverse".
+   *
+   * We don't know how many inverses we will need before DPLL(T) search,
+   * since we could get a new diseq at any time.
+   *
+   * We also have to tell CoCoA which variables we want before creating *any*
+   * CoCoA polynomials.
+   *
+   * So we guess a number of inverses, use them incrementally, and double the
+   * number (clearing all CoCoA polynomials) whenever we exceed the bound.
+   */
+  size_t d_numInverses = 10;
+
+  /**
+   * Statistics shared among all finite-field sub-theories.
+   */
   FfStatistics* d_stats;
-  // The base field of the multivariate polynomial ring.
-  //
-  // That is, the field that the polynomial coefficients live in/the
-  // finite-field constants live in.
-  //
-  // For now, we assume this is a prime-order finite-field.
+  /**
+   * The base field of the multivariate polynomial ring.
+   *
+   * That is, the field that the polynomial coefficients live in/the
+   * finite-field constants live in.
+   *
+   * For now, we assume this is a prime-order finite-field.
+   */
   CoCoA::ring d_baseRing;
-  // The prime modulus for the base field.
+  /**
+   * The prime modulus for the base field.
+   */
   Integer d_modulus;
-  // Set after registration is done.
+  /**
+   * Set after registration is done.
+   */
   std::optional<CoCoA::ring> d_polyRing{};
 };
 
diff --git a/src/theory/ff/theory_ff.cpp b/src/theory/ff/theory_ff.cpp
index 859742aa859..0f19e5da3d8 100644
--- a/src/theory/ff/theory_ff.cpp
+++ b/src/theory/ff/theory_ff.cpp
@@ -23,6 +23,7 @@
 #include <unordered_map>
 
 #include "expr/node_traversal.h"
+#include "options/ff_options.h"
 #include "theory/theory_model.h"
 #include "theory/trust_substitutions.h"
 #include "util/statistics_registry.h"
@@ -47,7 +48,9 @@ TheoryFiniteFields::TheoryFiniteFields(Env& env,
     : Theory(THEORY_FF, env, out, valuation),
       d_state(env, valuation),
       d_im(env, *this, d_state, getStatsPrefix(THEORY_FF)),
-      d_eqNotify(d_im)
+      d_eqNotify(d_im),
+      d_stats(
+          std::make_unique<FfStatistics>(statisticsRegistry(), "theory::ff::"))
 {
   d_theoryState = &d_state;
   d_inferManager = &d_im;
@@ -77,7 +80,22 @@ void TheoryFiniteFields::finishInit()
 
 void TheoryFiniteFields::postCheck(Effort level)
 {
-  // TODO
+#ifdef CVC5_USE_COCOA
+  Trace("ff::check") << "ff::check : " << level << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  for (auto& subTheory : d_subTheories)
+  {
+    subTheory.second.postCheck(level);
+    if (subTheory.second.inConflict())
+    {
+      d_im.conflict(
+          nm->mkAnd(subTheory.second.conflict()),
+          InferenceId::FF_LEMMA);
+    }
+  }
+#else  /* CVC5_USE_COCOA */
+  // We've received no facts (or we'd have crashed on notifyFact), so do nothing
+#endif /* CVC5_USE_COCOA */
 }
 
 void TheoryFiniteFields::notifyFact(TNode atom,
@@ -85,62 +103,81 @@ void TheoryFiniteFields::notifyFact(TNode atom,
                                     TNode fact,
                                     bool isInternal)
 {
-  // TODO
+#ifdef CVC5_USE_COCOA
+  Trace("ff::check") << "ff::notifyFact : " << fact << " @ level "
+                     << context()->getLevel() << std::endl;
+  d_subTheories.at(atom[0].getType()).notifyFact(fact);
+#else  /* CVC5_USE_COCOA */
+  noCoCoA();
+#endif /* CVC5_USE_COCOA */
 }
 
 bool TheoryFiniteFields::collectModelValues(TheoryModel* m,
                                             const std::set<Node>& termSet)
 {
-  // TODO
+#ifdef CVC5_USE_COCOA
+  Trace("ff::model") << "Term set: " << termSet << std::endl;
+  for (const auto& subTheory : d_subTheories)
+  {
+    for (const auto& entry : subTheory.second.model())
+    {
+      Trace("ff::model") << "Model entry: " << entry.first << " -> "
+                         << entry.second << std::endl;
+      if (termSet.count(entry.first))
+      {
+        bool okay = m->assertEquality(entry.first, entry.second, true);
+        Assert(okay) << "Our model was rejected";
+      }
+    }
+  }
+#else  /* CVC5_USE_COCOA */
+  // We've received no facts (or we'd have crashed on notifyFact), so do nothing
+#endif /* CVC5_USE_COCOA */
   return true;
 }
 
-void TheoryFiniteFields::computeCareGraph()
+void TheoryFiniteFields::preRegisterWithEe(TNode node)
 {
-  // TODO
-}
-
-TrustNode TheoryFiniteFields::explain(TNode node)
-{
-  // TODO
-  return TrustNode::null();
-}
-
-Node TheoryFiniteFields::getModelValue(TNode node)
-{
-  // TODO
-  return Node::null();
+  Assert(d_equalityEngine != nullptr);
+  if (node.getKind() == kind::EQUAL)
+  {
+    d_equalityEngine->addTriggerPredicate(node);
+  }
+  else
+  {
+    d_equalityEngine->addTerm(node);
+  }
 }
 
 void TheoryFiniteFields::preRegisterTerm(TNode node)
 {
-  // TODO
-}
-
-TrustNode TheoryFiniteFields::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
-{
-  // TODO
-  return TrustNode::null();
-}
-
-Theory::PPAssertStatus TheoryFiniteFields::ppAssert(
-    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
-{
-  TNode in = tin.getNode();
-  Trace("ff::pp") << "ff::ppAssert : " << in << std::endl;
-  Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
-  return status;
-}
-
-void TheoryFiniteFields::presolve()
-{
-  // TODO
+  preRegisterWithEe(node);
+#ifdef CVC5_USE_COCOA
+  Trace("ff::register") << "ff::preRegisterTerm : " << node << std::endl;
+  TypeNode ty = node.getType();
+  TypeNode fieldTy = ty;
+  if (!ty.isFiniteField())
+  {
+    Assert(node.getKind() == Kind::EQUAL);
+    fieldTy = node[0].getType();
+  }
+  if (d_subTheories.count(fieldTy) == 0)
+  {
+    d_subTheories.try_emplace(
+        fieldTy, d_env, d_stats.get(), ty.getFfSize());
+  }
+  d_subTheories.at(fieldTy).preRegisterTerm(node);
+#else  /* CVC5_USE_COCOA */
+  noCoCoA();
+#endif /* CVC5_USE_COCOA */
 }
 
-bool TheoryFiniteFields::isEntailed(Node n, bool pol)
+TrustNode TheoryFiniteFields::explain(TNode n)
 {
-  // TODO
-  return false;
+  Trace("ff::prop") << "explain " << n << std::endl;
+  TrustNode exp = d_im.explainLit(n);
+  AlwaysAssert(!exp.isNull());
+  return exp;
 }
 
 }  // namespace ff
diff --git a/src/theory/ff/theory_ff.h b/src/theory/ff/theory_ff.h
index 695cf0c4967..c9da318d434 100644
--- a/src/theory/ff/theory_ff.h
+++ b/src/theory/ff/theory_ff.h
@@ -10,7 +10,16 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Finite fields theory
+ * Finite fields theory.
+ *
+ * Overview:
+ *
+ * * There is a subtheory for each prime p that handles the field Fp
+ * * For each p, we build a polynomial ring Fp[X].
+ *   * X contains a variable for each theory leaf
+ *   * Facts become polynomials whose (common) roots are models.
+ *     * (= s t) is polynomial s - t
+ *     * (not (= s t)) is polynomial w(s - t) - 1 (with fresh w
  */
 
 #include "cvc5_private.h"
@@ -22,6 +31,8 @@
 
 #include "smt/logic_exception.h"
 #include "theory/care_pair_argument_callback.h"
+#include "theory/ff/stats.h"
+#include "theory/ff/sub_theory.h"
 #include "theory/ff/theory_ff_rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
@@ -55,24 +66,51 @@ class TheoryFiniteFields : public Theory
   //--------------------------------- end initialization
 
   //--------------------------------- standard check
-  /** Post-check, called after the fact queue of the theory is processed. */
+  /** Post-check, called after the fact queue of the theory is processed.
+   *
+   * For each sub-theory:
+   * 1. Ensure we have constructed Fp[X], with X that covers all theory leaves
+   *    and contains a fresh w for each disequality
+   * 2. Map all assertions to polynomials. Call the polynomial set P.
+   * 3. Use GB to check whether 1 is in the ideal generated by P. If so, UNSAT
+   *     * Extract a core from GB instrumentation.
+   * 4. Do search for model construction
+   *    * If some variable X0 has a univariate polynomial, find all roots and
+   *      branch on them
+   *    * If the ideal has dimension 0, choose a variable X0, construct the
+   *      (univariate) minimal polynomial for it, find all roots, and branch
+   *    * Do a round robin guess: X0 = 0, X1 = 0, .., Xk = 0, X0 = 1, X1 = 1,
+   *      ...
+   */
   void postCheck(Effort level) override;
-  /** Notify fact */
+  /**
+   * The subtheory saves this for later (postCheck)
+   * */
   void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
   //--------------------------------- end standard check
-  /** Collect model values in m based on the relevant terms given by termSet */
+  /**
+   * Lift the common polynomial root to a model
+   *
+   * * For each polynomial variable Xi (set to value V)
+   *   * if Xi corresponds to a theory variable in `termSet`
+   *     * assert it’s value is V
+   */
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
-  void computeCareGraph() override;
-  TrustNode explain(TNode) override;
-  Node getModelValue(TNode) override;
   std::string identify() const override { return "THEORY_FF"; }
+  /** preRegister this term or equality with the eq engine */
+  void preRegisterWithEe(TNode node);
+  /**
+   * Trigers the creation of new-subtheories, and used to track the variables of
+   * the polynomial ring that we will build.
+   *
+   * 1. Registers term with the equality engine
+   * 2. Creates a new sub-theory for this term’s sort (if needed)
+   * 3. Gives this term to that sub-theory
+   *   * Maintains a list of all theory leaves (for the variable set X)
+   */
   void preRegisterTerm(TNode node) override;
-  TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems) override;
-  PPAssertStatus ppAssert(TrustNode tin,
-                          TrustSubstitutionMap& outSubstitutions) override;
-  void presolve() override;
-  bool isEntailed(Node n, bool pol);
+  TrustNode explain(TNode n) override;
 
  private:
   TheoryFiniteFieldsRewriter d_rewriter{};
@@ -85,6 +123,15 @@ class TheoryFiniteFields : public Theory
 
   /** Manages notifications from our equality engine */
   TheoryEqNotifyClass d_eqNotify;
+
+#ifdef CVC5_USE_COCOA
+  /**
+   * Map from field types to sub-theories.
+   */
+  std::unordered_map<TypeNode, SubTheory> d_subTheories;
+#endif /* CVC5_USE_COCOA */
+
+  std::unique_ptr<FfStatistics> d_stats;
 }; /* class TheoryFiniteFields */
 
 }  // namespace ff
diff --git a/src/theory/ff/theory_ff_rewriter.cpp b/src/theory/ff/theory_ff_rewriter.cpp
index a19f355f07b..e198cf1296e 100644
--- a/src/theory/ff/theory_ff_rewriter.cpp
+++ b/src/theory/ff/theory_ff_rewriter.cpp
@@ -18,7 +18,7 @@
 #include "expr/algorithm/flatten.h"
 #include "expr/attribute.h"
 #include "expr/node_manager.h"
-#include "util/ff_val.h"
+#include "util/finite_field_value.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -43,17 +43,17 @@ Node mkNary(Kind k, std::vector<Node>&& children)
  *
  *  If there is no constant scalar, returns a 1.
  */
-std::pair<Node, FfVal> parseScalar(TNode t)
+std::pair<Node, FiniteFieldValue> parseScalar(TNode t)
 {
   const TypeNode field = t.getType();
   Assert(field.isFiniteField());
-  FfVal scalar = FfVal::mkOne(field.getFfSize());
+  FiniteFieldValue scalar = FiniteFieldValue::mkOne(field.getFfSize());
   Node node = t;
   if (t.getKind() == Kind::FINITE_FIELD_MULT && t[0].isConst())
   {
     std::vector<Node> restChildren(std::next(t.begin()), t.end());
     node = mkNary(Kind::FINITE_FIELD_MULT, std::move(restChildren));
-    scalar = t[0].getConst<FfVal>();
+    scalar = t[0].getConst<FiniteFieldValue>();
   }
   return {node, scalar};
 }
@@ -63,7 +63,7 @@ Node preRewriteFfNeg(TNode t)
 {
   Assert(t.getKind() == Kind::FINITE_FIELD_NEG);
   NodeManager* const nm = NodeManager::currentNM();
-  const Node negOne = nm->mkConst(FfVal(Integer(-1), t.getType().getFfSize()));
+  const Node negOne = nm->mkConst(FiniteFieldValue(Integer(-1), t.getType().getFfSize()));
   return nm->mkNode(kind::FINITE_FIELD_MULT, negOne, t[0]);
 }
 
@@ -80,10 +80,10 @@ Node postRewriteFfAdd(TNode t)
   const TypeNode field = t.getType();
   Assert(field.isFiniteField());
 
-  FfVal one = FfVal::mkOne(field.getFfSize());
+  FiniteFieldValue one = FiniteFieldValue::mkOne(field.getFfSize());
 
-  FfVal constantTerm = FfVal::mkZero(field.getFfSize());
-  std::map<Node, FfVal> scalarTerms;
+  FiniteFieldValue constantTerm = FiniteFieldValue::mkZero(field.getFfSize());
+  std::map<Node, FiniteFieldValue> scalarTerms;
 
   std::vector<TNode> children;
   expr::algorithm::flatten(t, children);
@@ -92,11 +92,11 @@ Node postRewriteFfAdd(TNode t)
   {
     if (child.isConst())
     {
-      constantTerm = constantTerm + child.getConst<FfVal>();
+      constantTerm = constantTerm + child.getConst<FiniteFieldValue>();
     }
     else
     {
-      std::pair<Node, FfVal> pair = parseScalar(child);
+      std::pair<Node, FiniteFieldValue> pair = parseScalar(child);
       auto entry = scalarTerms.find(pair.first);
       if (entry == scalarTerms.end())
       {
@@ -139,7 +139,7 @@ Node postRewriteFfAdd(TNode t)
   if (summands.size() == 0)
   {
     // again, this is possible through cancellation.
-    return nm->mkConst(FfVal::mkZero(field.getFfSize()));
+    return nm->mkConst(FiniteFieldValue::mkZero(field.getFfSize()));
   }
   return mkNary(Kind::FINITE_FIELD_ADD, std::move(summands));
 }
@@ -157,9 +157,9 @@ Node postRewriteFfMult(TNode t)
   const TypeNode field = t.getType();
   Assert(field.isFiniteField());
 
-  FfVal one = FfVal::mkOne(field.getFfSize());
+  FiniteFieldValue one = FiniteFieldValue::mkOne(field.getFfSize());
 
-  FfVal constantTerm = FfVal::mkOne(field.getFfSize());
+  FiniteFieldValue constantTerm = FiniteFieldValue::mkOne(field.getFfSize());
   std::vector<Node> factors;
 
   std::vector<TNode> children;
@@ -169,7 +169,7 @@ Node postRewriteFfMult(TNode t)
   {
     if (child.isConst())
     {
-      constantTerm = constantTerm * child.getConst<FfVal>();
+      constantTerm = constantTerm * child.getConst<FiniteFieldValue>();
     }
     else
     {
@@ -194,8 +194,8 @@ Node postRewriteFfEq(TNode t)
   Assert(t.getKind() == Kind::EQUAL);
   if (t[0].isConst() && t[1].isConst())
   {
-    FfVal l = t[0].getConst<FfVal>();
-    FfVal r = t[1].getConst<FfVal>();
+    FiniteFieldValue l = t[0].getConst<FiniteFieldValue>();
+    FiniteFieldValue r = t[1].getConst<FiniteFieldValue>();
     return NodeManager::currentNM()->mkConst<bool>(l == r);
   }
   else if (t[0] == t[1])
diff --git a/src/theory/ff/theory_ff_rewriter.h b/src/theory/ff/theory_ff_rewriter.h
index 6ea762174ea..8ec53d8e25a 100644
--- a/src/theory/ff/theory_ff_rewriter.h
+++ b/src/theory/ff/theory_ff_rewriter.h
@@ -23,7 +23,7 @@
 
 #include "expr/node.h"
 #include "theory/rewriter.h"
-#include "util/ff_val.h"
+#include "util/finite_field_value.h"
 
 namespace cvc5::internal {
 namespace theory {
diff --git a/src/theory/ff/theory_ff_type_rules.cpp b/src/theory/ff/theory_ff_type_rules.cpp
index 3dcf876a2a9..8b30ff8eadb 100644
--- a/src/theory/ff/theory_ff_type_rules.cpp
+++ b/src/theory/ff/theory_ff_type_rules.cpp
@@ -16,7 +16,7 @@
 #include "theory/ff/theory_ff_type_rules.h"
 
 #include "util/cardinality.h"
-#include "util/ff_val.h"
+#include "util/finite_field_value.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -36,7 +36,7 @@ TypeNode FiniteFieldConstantTypeRule::computeType(NodeManager* nodeManager,
                                                   bool _check)
 {
   return nodeManager->mkFiniteFieldType(
-      n.getConst<FfVal>().getFieldSize());
+      n.getConst<FiniteFieldValue>().getFieldSize());
 }
 
 TypeNode FiniteFieldFixedFieldTypeRule::computeType(NodeManager* nodeManager,
diff --git a/src/theory/ff/type_enumerator.h b/src/theory/ff/type_enumerator.h
index 6908cc08599..a910882754b 100644
--- a/src/theory/ff/type_enumerator.h
+++ b/src/theory/ff/type_enumerator.h
@@ -21,7 +21,7 @@
 #include "expr/kind.h"
 #include "expr/type_node.h"
 #include "theory/type_enumerator.h"
-#include "util/ff_val.h"
+#include "util/finite_field_value.h"
 #include "util/integer.h"
 
 namespace cvc5::internal {
@@ -49,8 +49,8 @@ class FiniteFieldEnumerator : public TypeEnumeratorBase<FiniteFieldEnumerator>
     {
       throw NoMoreValuesException(getType());
     }
-    return NodeManager::currentNM()->mkConst<FfVal>(
-        FfVal(d_currentInt, d_modulus));
+    return NodeManager::currentNM()->mkConst<FiniteFieldValue>(
+        FiniteFieldValue(d_currentInt, d_modulus));
   }
 
   FiniteFieldEnumerator& operator++() override
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 2c6faa915e8..0809968e400 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -109,6 +109,7 @@ const char* toString(InferenceId i)
     case InferenceId::ARITH_NL_ICP_CONFLICT: return "ARITH_NL_ICP_CONFLICT";
     case InferenceId::ARITH_NL_ICP_PROPAGATION:
       return "ARITH_NL_ICP_PROPAGATION";
+    case InferenceId::FF_LEMMA: return "FF_LEMMA";
 
     case InferenceId::ARRAYS_EXT: return "ARRAYS_EXT";
     case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index d8a42bf99d9..56e96578392 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -172,8 +172,14 @@ enum class InferenceId
   ARITH_NL_ICP_CONFLICT,
   // propagation / contraction of variable bounds from icp
   ARITH_NL_ICP_PROPAGATION,
+  //-------------------- ff inference
   // ---------------------------------- end arith theory
 
+  // ---------------------------------- finite field theory
+  // a catch-all, for now
+  FF_LEMMA,
+  // ---------------------------------- end finite field theory
+
   // ---------------------------------- arrays theory
   ARRAYS_EXT,
   ARRAYS_READ_OVER_WRITE,
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 3aa43f1b374..eacde20e1c7 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -21,8 +21,8 @@ libcvc5_add_sources(
   bin_heap.h
   bitvector.cpp
   bitvector.h
-  ff_val.cpp
-  ff_val.h
+  cocoa_globals.cpp
+  cocoa_globals.h
   bool.h
   cardinality.cpp
   cardinality.h
@@ -35,6 +35,8 @@ libcvc5_add_sources(
   didyoumean.h
   divisible.cpp
   divisible.h
+  finite_field_value.cpp
+  finite_field_value.h
   floatingpoint.cpp
   floatingpoint.h
   floatingpoint_size.cpp
diff --git a/src/util/ff_val.cpp b/src/util/finite_field_value.cpp
similarity index 64%
rename from src/util/ff_val.cpp
rename to src/util/finite_field_value.cpp
index 6a06d4ec490..1c5e72675bc 100644
--- a/src/util/ff_val.cpp
+++ b/src/util/finite_field_value.cpp
@@ -13,30 +13,30 @@
  * A finite-field element, implemented as a wrapper around Integer.
  */
 
-#include "util/ff_val.h"
+#include "util/finite_field_value.h"
 
 #include "util/hash.h"
 
 namespace cvc5::internal {
 
-const Integer& FfVal::getValue() const { return d_value; }
+const Integer& FiniteFieldValue::getValue() const { return d_value; }
 
-const Integer& FfVal::getFieldSize() const { return d_size; }
+const Integer& FiniteFieldValue::getFieldSize() const { return d_size; }
 
-Integer FfVal::toInteger() const { return d_value; }
+Integer FiniteFieldValue::toInteger() const { return d_value; }
 
-Integer FfVal::toSignedInteger() const
+Integer FiniteFieldValue::toSignedInteger() const
 {
   Integer half_size = d_size.divByPow2(1) + 1;
   return (d_value < half_size) ? d_value : d_value - d_size;
 }
 
-std::string FfVal::toString() const
+std::string FiniteFieldValue::toString() const
 {
   return toSignedInteger().toString();
 }
 
-size_t FfVal::hash() const
+size_t FiniteFieldValue::hash() const
 {
   PairHashFunction<size_t, size_t> h;
   return h(std::make_pair(d_value.hash(), d_size.hash()));
@@ -48,13 +48,13 @@ size_t FfVal::hash() const
 
 /* (Dis)Equality --------------------------------------------------------- */
 
-bool operator==(const FfVal& x, const FfVal& y)
+bool operator==(const FiniteFieldValue& x, const FiniteFieldValue& y)
 {
   if (x.d_size != y.d_size) return false;
   return x.d_value == y.d_value;
 }
 
-bool operator!=(const FfVal& x, const FfVal& y)
+bool operator!=(const FiniteFieldValue& x, const FiniteFieldValue& y)
 {
   if (x.d_size != y.d_size) return true;
   return x.d_value != y.d_value;
@@ -62,29 +62,29 @@ bool operator!=(const FfVal& x, const FfVal& y)
 
 /* Unsigned Inequality --------------------------------------------------- */
 
-bool operator<(const FfVal& x, const FfVal& y)
+bool operator<(const FiniteFieldValue& x, const FiniteFieldValue& y)
 {
   return x.d_value < y.d_value;
 }
 
-bool operator<=(const FfVal& x, const FfVal& y)
+bool operator<=(const FiniteFieldValue& x, const FiniteFieldValue& y)
 {
   return x.d_value <= y.d_value;
 }
 
-bool operator>(const FfVal& x, const FfVal& y)
+bool operator>(const FiniteFieldValue& x, const FiniteFieldValue& y)
 {
   return x.d_value > y.d_value;
 }
 
-bool operator>=(const FfVal& x, const FfVal& y)
+bool operator>=(const FiniteFieldValue& x, const FiniteFieldValue& y)
 {
   return x.d_value >= y.d_value;
 }
 
 /* Arithmetic operations ------------------------------------------------- */
 
-FfVal operator+(const FfVal& x, const FfVal& y)
+FiniteFieldValue operator+(const FiniteFieldValue& x, const FiniteFieldValue& y)
 {
   Assert(x.d_size == y.d_size)
       << "Size mismatch: " << x.d_size << " != " << y.d_size;
@@ -92,19 +92,19 @@ FfVal operator+(const FfVal& x, const FfVal& y)
   return {sum, x.d_size};
 }
 
-FfVal operator-(const FfVal& x, const FfVal& y)
+FiniteFieldValue operator-(const FiniteFieldValue& x, const FiniteFieldValue& y)
 {
   Assert(x.d_size == y.d_size)
       << "Size mismatch: " << x.d_size << " != " << y.d_size;
   return {x.d_value - y.d_value, x.d_size};
 }
 
-FfVal operator-(const FfVal& x)
+FiniteFieldValue operator-(const FiniteFieldValue& x)
 {
   return {x.d_size - x.d_value, x.d_size};
 }
 
-FfVal operator*(const FfVal& x, const FfVal& y)
+FiniteFieldValue operator*(const FiniteFieldValue& x, const FiniteFieldValue& y)
 {
   Assert(x.d_size == y.d_size)
       << "Size mismatch: " << x.d_size << " != " << y.d_size;
@@ -112,12 +112,12 @@ FfVal operator*(const FfVal& x, const FfVal& y)
   return {prod, x.d_size};
 }
 
-FfVal operator/(const FfVal& x, const FfVal& y)
+FiniteFieldValue operator/(const FiniteFieldValue& x, const FiniteFieldValue& y)
 {
   return x * y.recip();
 }
 
-FfVal FfVal::recip() const
+FiniteFieldValue FiniteFieldValue::recip() const
 {
   Assert(!d_value.isZero());
   return {d_value.modInverse(d_size), d_size};
@@ -127,7 +127,7 @@ FfVal FfVal::recip() const
  * Output stream
  * ----------------------------------------------------------------------- */
 
-std::ostream& operator<<(std::ostream& os, const FfVal& ff)
+std::ostream& operator<<(std::ostream& os, const FiniteFieldValue& ff)
 {
   return os << ff.toString();
 }
@@ -136,8 +136,8 @@ std::ostream& operator<<(std::ostream& os, const FfVal& ff)
  * Static helpers.
  * ----------------------------------------------------------------------- */
 
-FfVal FfVal::mkZero(const Integer& size) { return {0, size}; }
+FiniteFieldValue FiniteFieldValue::mkZero(const Integer& size) { return {0, size}; }
 
-FfVal FfVal::mkOne(const Integer& size) { return {1, size}; }
+FiniteFieldValue FiniteFieldValue::mkOne(const Integer& size) { return {1, size}; }
 
 }  // namespace cvc5::internal
diff --git a/src/util/ff_val.h b/src/util/finite_field_value.h
similarity index 55%
rename from src/util/ff_val.h
rename to src/util/finite_field_value.h
index 5f647cb9ac0..e30297a5c52 100644
--- a/src/util/ff_val.h
+++ b/src/util/finite_field_value.h
@@ -13,14 +13,15 @@
  * A finite-field element, implemented as a wrapper around Integer.
  *
  * TODOs:
- * * consider montgomery form
  * * extend to non-prime fields
+ * (https://github.com/cvc5/cvc5-wishues/issues/139)
+ * * consider montgomery form (https://github.com/cvc5/cvc5-wishues/issues/140)
  */
 
 #include "cvc5_public.h"
 
-#ifndef CVC5__FINITE_FIELD_H
-#define CVC5__FINITE_FIELD_H
+#ifndef CVC5__FINITE_FIELDVALUE_H
+#define CVC5__FINITE_FIELDVALUE_H
 
 #include <iosfwd>
 
@@ -30,10 +31,10 @@
 
 namespace cvc5::internal {
 
-class FfVal
+class FiniteFieldValue
 {
  public:
-  FfVal(const Integer& val, const Integer& size)
+  FiniteFieldValue(const Integer& val, const Integer& size)
       : d_size(size),
         // normalize value into [0, size)
         d_value(val.floorDivideRemainder(size))
@@ -45,15 +46,15 @@ class FfVal
   /**
    * Construct the zero in this field
    */
-  FfVal(const Integer& size) : d_size(size), d_value(0)
+  FiniteFieldValue(const Integer& size) : d_size(size), d_value(0)
   {
     // we only support prime fields right now
     Assert(size.isProbablePrime());
   }
 
-  ~FfVal() {}
+  ~FiniteFieldValue() {}
 
-  FfVal& operator=(const FfVal& x)
+  FiniteFieldValue& operator=(const FiniteFieldValue& x)
   {
     if (this == &x)
     {
@@ -86,30 +87,34 @@ class FfVal
   /* Return hash value. */
   size_t hash() const;
 
-  friend bool operator==(const FfVal&, const FfVal&);
-  friend bool operator!=(const FfVal&, const FfVal&);
-  friend bool operator<(const FfVal&, const FfVal&);
-  friend bool operator>(const FfVal&, const FfVal&);
-  friend bool operator>=(const FfVal&, const FfVal&);
-  friend bool operator<=(const FfVal&, const FfVal&);
-  friend FfVal operator+(const FfVal&, const FfVal&);
-  friend FfVal operator-(const FfVal&, const FfVal&);
-  friend FfVal operator-(const FfVal&);
-  friend FfVal operator*(const FfVal&, const FfVal&);
-  friend FfVal operator/(const FfVal&, const FfVal&);
+  friend bool operator==(const FiniteFieldValue&, const FiniteFieldValue&);
+  friend bool operator!=(const FiniteFieldValue&, const FiniteFieldValue&);
+  friend bool operator<(const FiniteFieldValue&, const FiniteFieldValue&);
+  friend bool operator>(const FiniteFieldValue&, const FiniteFieldValue&);
+  friend bool operator>=(const FiniteFieldValue&, const FiniteFieldValue&);
+  friend bool operator<=(const FiniteFieldValue&, const FiniteFieldValue&);
+  friend FiniteFieldValue operator+(const FiniteFieldValue&,
+                                    const FiniteFieldValue&);
+  friend FiniteFieldValue operator-(const FiniteFieldValue&,
+                                    const FiniteFieldValue&);
+  friend FiniteFieldValue operator-(const FiniteFieldValue&);
+  friend FiniteFieldValue operator*(const FiniteFieldValue&,
+                                    const FiniteFieldValue&);
+  friend FiniteFieldValue operator/(const FiniteFieldValue&,
+                                    const FiniteFieldValue&);
 
   /* Reciprocal. Crashes on 0. */
-  FfVal recip() const;
+  FiniteFieldValue recip() const;
 
   /* -----------------------------------------------------------------------
    ** Static helpers.
    * ----------------------------------------------------------------------- */
 
   /* Create zero bit-vector of given size. */
-  static FfVal mkZero(const Integer& modulus);
+  static FiniteFieldValue mkZero(const Integer& modulus);
 
   /* Create bit-vector representing value 1 of given size. */
-  static FfVal mkOne(const Integer& modulus);
+  static FiniteFieldValue mkOne(const Integer& modulus);
 
  private:
   /**
@@ -121,38 +126,36 @@ class FfVal
   Integer d_size;
   Integer d_value;
 
-}; /* class FfVal */
+}; /* class FiniteFieldValue */
 
 struct FfSize
 {
-  FfSize(Integer size) : d_size(size) {}
-  operator const Integer&() const { return d_size; }
-  bool operator==(const FfSize& y) const
+  FfSize(Integer size) : d_size(size)
   {
-    return d_size == y.d_size;
+    // we only support prime fields right now
+    Assert(size.isProbablePrime());
   }
-  
+  operator const Integer&() const { return d_size; }
+  bool operator==(const FfSize& y) const { return d_size == y.d_size; }
+
   Integer d_size;
 }; /* struct FfSize */
 
 /*
- * Hash function for the FfVal.
+ * Hash function for the FiniteFieldValue.
  */
-struct FfValHashFunction
+struct FiniteFieldValueHashFunction
 {
-  size_t operator()(const FfVal& ff) const { return ff.hash(); }
-}; /* struct FfValHashFunction */
+  size_t operator()(const FiniteFieldValue& ff) const { return ff.hash(); }
+}; /* struct FiniteFieldValueHashFunction */
 
 /*
  * Hash function for the FfSize constants.
  */
 struct FfSizeHashFunction
 {
-  size_t operator()(const FfSize& size) const
-  {
-    return size.d_size.hash();
-  }
-}; /* struct FfValHashFunction */
+  size_t operator()(const FfSize& size) const { return size.d_size.hash(); }
+}; /* struct FiniteFieldValueHashFunction */
 
 /* -----------------------------------------------------------------------
  ** Operators
@@ -161,48 +164,52 @@ struct FfSizeHashFunction
 /* (Dis)Equality --------------------------------------------------------- */
 
 /* Return true if x is equal to 'y'. */
-bool operator==(const FfVal& x, const FfVal& y);
+bool operator==(const FiniteFieldValue& x, const FiniteFieldValue& y);
 
 /* Return true if x is not equal to 'y'. */
-bool operator!=(const FfVal& x, const FfVal& y);
+bool operator!=(const FiniteFieldValue& x, const FiniteFieldValue& y);
 
 /* Unsigned Inequality --------------------------------------------------- */
 
 /* Return true if x is unsigned less than finite field 'y'. */
-bool operator<(const FfVal& x, const FfVal& y);
+bool operator<(const FiniteFieldValue& x, const FiniteFieldValue& y);
 
 /* Return true if x is unsigned less than or equal to finite field 'y'. */
-bool operator<=(const FfVal& x, const FfVal& y);
+bool operator<=(const FiniteFieldValue& x, const FiniteFieldValue& y);
 
 /* Return true if x is unsigned greater than finite field 'y'. */
-bool operator>(const FfVal& x, const FfVal& y);
+bool operator>(const FiniteFieldValue& x, const FiniteFieldValue& y);
 
 /* Return true if x is unsigned greater than or equal to finite field 'y'. */
-bool operator>=(const FfVal& x, const FfVal& y);
+bool operator>=(const FiniteFieldValue& x, const FiniteFieldValue& y);
 
 /* Arithmetic operations ------------------------------------------------- */
 
 /* Return a finite field representing the addition (x + y). */
-FfVal operator+(const FfVal& x, const FfVal& y);
+FiniteFieldValue operator+(const FiniteFieldValue& x,
+                           const FiniteFieldValue& y);
 
 /* Return a finite field representing the subtraction (x - y). */
-FfVal operator-(const FfVal& x, const FfVal& y);
+FiniteFieldValue operator-(const FiniteFieldValue& x,
+                           const FiniteFieldValue& y);
 
 /* Return a finite field representing the negation of x. */
-FfVal operator-(const FfVal& x);
+FiniteFieldValue operator-(const FiniteFieldValue& x);
 
 /* Return a finite field representing the multiplication (x * y). */
-FfVal operator*(const FfVal& x, const FfVal& y);
+FiniteFieldValue operator*(const FiniteFieldValue& x,
+                           const FiniteFieldValue& y);
 
 /* Return a finite field representing the division (x / y). */
-FfVal operator/(const FfVal& x, const FfVal& y);
+FiniteFieldValue operator/(const FiniteFieldValue& x,
+                           const FiniteFieldValue& y);
 
 /* -----------------------------------------------------------------------
  * Output stream
  * ----------------------------------------------------------------------- */
 
-std::ostream& operator<<(std::ostream& os, const FfVal& ff);
+std::ostream& operator<<(std::ostream& os, const FiniteFieldValue& ff);
 
 }  // namespace cvc5::internal
 
-#endif /* CVC5__FINITE_FIELD_H */
+#endif /* CVC5__FINITE_FIELDVALUE_H */
diff --git a/test/api/cpp/finite_field.cpp b/test/api/cpp/finite_field.cpp
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt
index 439b96bfd7c..27d2e0fd5c0 100644
--- a/test/api/python/CMakeLists.txt
+++ b/test/api/python/CMakeLists.txt
@@ -30,6 +30,9 @@ endmacro()
 
 # add specific test files
 cvc5_add_python_api_test(pyapi_boilerplate boilerplate.py)
+if(USE_COCOA)
+  cvc5_add_python_api_test(pyapi_finite_field finite_field.py)
+endif()
 cvc5_add_python_api_test(pyapi_issue4889 issue4889.py)
 cvc5_add_python_api_test(pyapi_issue5074 issue5074.py)
 cvc5_add_python_api_test(pyapi_issue6111 issue6111.py)
diff --git a/test/api/python/finite_field.py b/test/api/python/finite_field.py
new file mode 100644
index 00000000000..0e8361b12f8
--- /dev/null
+++ b/test/api/python/finite_field.py
@@ -0,0 +1,54 @@
+###############################################################################
+# Top contributors (to current version):
+#   Andrew Reynolds, Alex Ozdemir
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# A simple start-up/tear-down test for cvc5.
+#
+# This simple test just makes sure that the public interface is
+# minimally functional.  It is useful as a template to use for other
+# system tests.
+##
+
+import cvc5
+from cvc5 import Kind
+
+slv = cvc5.Solver()
+slv.setOption("produce-models", "true")
+F = slv.mkFiniteFieldSort(5)
+a = slv.mkConst(F, "a")
+b = slv.mkConst(F, "b")
+assert 5 == F.getFiniteFieldSize()
+
+inv = slv.mkTerm(
+    Kind.EQUAL,
+    slv.mkTerm(Kind.FINITE_FIELD_MULT, a, b),
+    slv.mkFiniteFieldElem(1, F),
+)
+aIsTwo = slv.mkTerm(
+    Kind.EQUAL,
+    a,
+    slv.mkFiniteFieldElem(2, F),
+)
+slv.assertFormula(inv)
+slv.assertFormula(aIsTwo)
+r = slv.checkSat()
+assert r.isSat()
+assert slv.getValue(a).toPythonObj() == 2
+assert slv.getValue(b).toPythonObj() == -2
+
+bIsTwo = slv.mkTerm(
+    Kind.EQUAL,
+    b,
+    slv.mkFiniteFieldElem(2, F),
+)
+slv.assertFormula(bIsTwo)
+r = slv.checkSat()
+assert not r.isSat()
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index cbbc2ab4fd7..dd09e9043e2 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -651,6 +651,37 @@ set(regress_0_tests
   regress0/expect/scrub.06.cvc.smt2
   regress0/expect/scrub.08.sy
   regress0/expect/scrub.09.p
+  regress0/ff/as.smt2
+  regress0/ff/bigff_is_zero_sound.smt2
+  regress0/ff/bigff_is_zero_unsound.smt2
+  regress0/ff/bool_nary_or_sound.smt2
+  regress0/ff/bool_nary_or_unsound.smt2
+  regress0/ff/combination.smt2
+  regress0/ff/ctx.smt2
+  regress0/ff/ff_is_zero_sound.smt2
+  regress0/ff/ff_is_zero_unsound.smt2
+  regress0/ff/ff_xor_sound.smt2
+  regress0/ff/ff_xor_unsound.smt2
+  regress0/ff/ff_xor_unsound_model.smt2
+  regress0/ff/multicheck.smt2
+  regress0/ff/negneg.smt2
+  regress0/ff/randcompile-sound-3i-5t-circ.smt2
+  regress0/ff/randcompile-sound-3i-5t-zokcirc.smt2
+  regress0/ff/randcompile-sound-3i-5t-zokref.smt2
+  regress0/ff/rewriter.smt2
+  regress0/ff/simple.smt2
+  regress0/ff/univar_conjunction_sat.smt2
+  regress0/ff/univar_conjunction_unsat.smt2
+  regress0/ff/with_uf.smt2
+  regress0/ff/with_uf2.smt2
+  regress0/ff/with_uf3.smt2
+  regress0/ff/with_uf4.smt2
+  regress0/ff/with_uf5.smt2
+  regress0/ff/with_uf6.smt2
+  regress0/ff/with_uf7.smt2
+  regress0/ff/with_uf8.smt2
+  regress0/ff/with_uf9.smt2
+  regress0/ff/xor_unsound_missing.smt2
   regress0/flet.smtv1.smt2
   regress0/flet2.smtv1.smt2
   regress0/fmf/array_card.smt2
diff --git a/test/regress/cli/regress0/ff/as.smt2 b/test/regress/cli/regress0/ff/as.smt2
new file mode 100644
index 00000000000..946e6b33e29
--- /dev/null
+++ b/test/regress/cli/regress0/ff/as.smt2
@@ -0,0 +1,10 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+; Tests the ff rewriter
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+; all disjuncts should be false
+(define-sort F () (_ FiniteField 17))
+(assert (= (as ff0 F) (ff.add (as ff1 F) (ff.neg (as ff1 F)))))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/bigff_is_zero_sound.smt2 b/test/regress/cli/regress0/ff/bigff_is_zero_sound.smt2
new file mode 100644
index 00000000000..377864be5e4
--- /dev/null
+++ b/test/regress/cli/regress0/ff/bigff_is_zero_sound.smt2
@@ -0,0 +1,21 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+; x, m, is_zero: field
+; The constraints mx - 1 + is_zero = 0
+;                 is_zero*x = 0
+; Imply that is_zero is zero or one and = (x == 0)
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+(define-sort F () (_ FiniteField 4002409555221667393417789825735904156556882819939007885332058136124031650490837864442687629129015664037894272559787))
+(declare-fun x () F)
+(declare-fun m () F)
+(declare-fun is_zero () F)
+(assert (not (=>
+  (and (= (as ff0 F)
+          (ff.add (ff.mul m x) (ff.neg (as ff1 F)) is_zero))
+       (= (as ff0 F) (ff.mul is_zero x)))
+  (and (or (= (as ff0 F) is_zero) (= (as ff1 F) is_zero))
+       (= (= (as ff1 F) is_zero) (= x (as ff0 F))))
+)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/bigff_is_zero_unsound.smt2 b/test/regress/cli/regress0/ff/bigff_is_zero_unsound.smt2
new file mode 100644
index 00000000000..cca22c722db
--- /dev/null
+++ b/test/regress/cli/regress0/ff/bigff_is_zero_unsound.smt2
@@ -0,0 +1,21 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+; x, m, is_zero: field
+; The constraints mx - 1 + is_zero = 0
+;                 is_zero*m = 0                     ;; Note: this *should* be is_zero*x=0
+; Imply that is_zero is zero or one and = (x == 0)
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+(define-sort F () (_ FiniteField 4002409555221667393417789825735904156556882819939007885332058136124031650490837864442687629129015664037894272559787))
+(declare-fun x () F)
+(declare-fun m () F)
+(declare-fun is_zero () F)
+(assert (not (=>
+  (and (= (as ff0 F)
+          (ff.add (ff.mul m x) (ff.neg (as ff1 F)) is_zero))
+       (= (as ff0 F) (ff.mul is_zero m)))
+  (and (or (= (as ff0 F) is_zero) (= (as ff1 F) is_zero))
+       (= (= (as ff1 F) is_zero) (= x (as ff0 F))))
+)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/bool_nary_or_sound.smt2 b/test/regress/cli/regress0/ff/bool_nary_or_sound.smt2
new file mode 100644
index 00000000000..3da44fde87b
--- /dev/null
+++ b/test/regress/cli/regress0/ff/bool_nary_or_sound.smt2
@@ -0,0 +1,18 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert (not (=
+  (or a b c)
+  (not (= (ff.add
+    (ite a #f1m5 #f0m5)
+    (ite b #f1m5 #f0m5)
+    (ite c #f1m5 #f0m5)
+  ) #f0m5
+  ))
+)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/bool_nary_or_unsound.smt2 b/test/regress/cli/regress0/ff/bool_nary_or_unsound.smt2
new file mode 100644
index 00000000000..a0d33c5e8ad
--- /dev/null
+++ b/test/regress/cli/regress0/ff/bool_nary_or_unsound.smt2
@@ -0,0 +1,22 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(declare-fun e () Bool)
+(assert (not (=
+  (or a b c d e)
+  (not (= (ff.add
+    (ite a #f1m5 #f0m5)
+    (ite b #f1m5 #f0m5)
+    (ite c #f1m5 #f0m5)
+    (ite d #f1m5 #f0m5)
+    (ite e #f1m5 #f0m5)
+  ) #f0m5
+  ))
+)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/combination.smt2 b/test/regress/cli/regress0/ff/combination.smt2
new file mode 100644
index 00000000000..85d163889af
--- /dev/null
+++ b/test/regress/cli/regress0/ff/combination.smt2
@@ -0,0 +1,22 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+; Tests the ff rewriter
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+; all disjuncts should be false
+(define-sort F3 () (_ FiniteField 3))
+(define-sort F5 () (_ FiniteField 5))
+(declare-fun a () F3)
+(declare-fun b () F5)
+(assert (or (= (ff.mul
+    (ff.add a (ff.neg (as ff0 F3)))
+    (ff.add a (ff.neg (as ff1 F3)))
+    (ff.add a (ff.neg (as ff2 F3)))
+    ) (as ff1 F3))
+(= (ff.mul
+    (ff.add b (ff.neg (as ff0 F5)))
+    (ff.add b (ff.neg (as ff1 F5)))
+    (ff.add b (ff.neg (as ff2 F5)))
+    ) (as ff1 F5))))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/ctx.smt2 b/test/regress/cli/regress0/ff/ctx.smt2
new file mode 100644
index 00000000000..005bcc85a72
--- /dev/null
+++ b/test/regress/cli/regress0/ff/ctx.smt2
@@ -0,0 +1,30 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: sat
+; COMMAND-LINE: --incremental
+; Tests the ff rewriter
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+; all disjuncts should be false
+(define-sort F () (_ FiniteField 17))
+(declare-fun a () F)
+(declare-fun b () F)
+(assert (= (ff.mul a a) b))
+(assert (= a (as ff1 F)))
+(check-sat)
+(push)
+(declare-fun c () F)
+(assert (= (ff.mul c c) c))
+(assert (= (ff.mul c c) (ff.mul (as ff2 F) b)))
+(check-sat)
+(pop)
+(push)
+(declare-fun c () F)
+(assert (= (ff.mul c c) c))
+(assert (= (ff.mul c c) b))
+(check-sat)
+(check-sat)
+(pop)
diff --git a/test/regress/cli/regress0/ff/ff_is_zero_sound.smt2 b/test/regress/cli/regress0/ff/ff_is_zero_sound.smt2
new file mode 100644
index 00000000000..5c96732b399
--- /dev/null
+++ b/test/regress/cli/regress0/ff/ff_is_zero_sound.smt2
@@ -0,0 +1,19 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+; x, m, is_zero: field
+; The constraints mx - 1 + is_zero = 0
+;                 is_zero*x = 0
+; Imply that is_zero is zero or one and = (x == 0)
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+(declare-fun x () (_ FiniteField 17))
+(declare-fun m () (_ FiniteField 17))
+(declare-fun is_zero () (_ FiniteField 17))
+(assert (not (=>
+  (and (= #f0m17 (ff.add (ff.mul m x) #f16m17 is_zero))
+       (= #f0m17 (ff.mul is_zero x)))
+  (and (or (= #f0m17 is_zero) (= #f1m17 is_zero))
+       (= (= #f1m17 is_zero) (= x #f0m17)))
+)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/ff_is_zero_unsound.smt2 b/test/regress/cli/regress0/ff/ff_is_zero_unsound.smt2
new file mode 100644
index 00000000000..bbe72bb0b4d
--- /dev/null
+++ b/test/regress/cli/regress0/ff/ff_is_zero_unsound.smt2
@@ -0,0 +1,20 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+; COMMAND-LINE: --no-debug-check-models
+; x, m, is_zero: field
+; The constraints mx - 1 + is_zero = 0
+;                 is_zero*m = 0                     ;; Note: this *should* be is_zero*x=0
+; Imply that is_zero is zero or one and = (x == 0)
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+(declare-fun x () (_ FiniteField 17))
+(declare-fun m () (_ FiniteField 17))
+(declare-fun is_zero () (_ FiniteField 17))
+(assert (not (=>
+  (and (= #f0m17 (ff.add (ff.mul m x) #f16m17 is_zero))
+       (= #f0m17 (ff.mul is_zero m)))
+  (and (or (= #f0m17 is_zero) (= #f1m17 is_zero))
+       (= (= #f1m17 is_zero) (= x #f0m17)))
+)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/ff_xor_sound.smt2 b/test/regress/cli/regress0/ff/ff_xor_sound.smt2
new file mode 100644
index 00000000000..b7c58af4313
--- /dev/null
+++ b/test/regress/cli/regress0/ff/ff_xor_sound.smt2
@@ -0,0 +1,37 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+; COMMAND-LINE: --no-debug-check-models
+; XOR compilation strategy (sound case)
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+(declare-fun f0 () (_ FiniteField 11))
+(declare-fun f1 () (_ FiniteField 11))
+(declare-fun f2 () (_ FiniteField 11))
+(declare-fun f3 () (_ FiniteField 11))
+(declare-fun sum () (_ FiniteField 11))
+(declare-fun d0 () (_ FiniteField 11))
+(declare-fun d1 () (_ FiniteField 11))
+(declare-fun d2 () (_ FiniteField 11))
+(declare-fun b0 () Bool)
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(declare-fun b3 () Bool)
+(define-fun b_to_f ((b Bool)) (_ FiniteField 11) (ite b #f1m11 #f0m11))
+(define-fun f_to_b ((f (_ FiniteField 11))) Bool (not (= f #f0m11)))
+(define-fun is_bit ((f (_ FiniteField 11))) Bool (or (= f #f0m11) (= f #f1m11)))
+(declare-fun m () (_ FiniteField 11))
+(declare-fun is_zero () (_ FiniteField 11))
+(assert (not (=>
+  (and (is_bit f0)
+       (is_bit f1)
+       (is_bit f2)
+       (is_bit f3)
+       (= (ff.add f0 f1 f2 f3) sum)
+       (= (ff.add d0 (ff.mul #f2m11 d1) (ff.mul #f4m11 d2)) sum)
+       (is_bit d0)
+       (is_bit d1)
+       (is_bit d2))
+  (= (f_to_b d0) (xor (f_to_b f0) (f_to_b f1) (f_to_b f2) (f_to_b f3)))
+)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/ff_xor_unsound.smt2 b/test/regress/cli/regress0/ff/ff_xor_unsound.smt2
new file mode 100644
index 00000000000..1326510b289
--- /dev/null
+++ b/test/regress/cli/regress0/ff/ff_xor_unsound.smt2
@@ -0,0 +1,38 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+; COMMAND-LINE: --no-debug-check-models
+; XOR compilation strategy (unsound because even though the XOR sum can not
+; overflow, the bit decomposition sum can.
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+(declare-fun f0 () (_ FiniteField 5))
+(declare-fun f1 () (_ FiniteField 5))
+(declare-fun f2 () (_ FiniteField 5))
+(declare-fun f3 () (_ FiniteField 5))
+(declare-fun sum () (_ FiniteField 5))
+(declare-fun d0 () (_ FiniteField 5))
+(declare-fun d1 () (_ FiniteField 5))
+(declare-fun d2 () (_ FiniteField 5))
+(declare-fun b0 () Bool)
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(declare-fun b3 () Bool)
+(define-fun b_to_f ((b Bool)) (_ FiniteField 5) (ite b #f1m5 #f0m5))
+(define-fun f_to_b ((f (_ FiniteField 5))) Bool (not (= f #f0m5)))
+(define-fun is_bit ((f (_ FiniteField 5))) Bool (or (= f #f0m5) (= f #f1m5)))
+(declare-fun m () (_ FiniteField 5))
+(declare-fun is_zero () (_ FiniteField 5))
+(assert (not (=>
+  (and (is_bit f0)
+       (is_bit f1)
+       (is_bit f2)
+       (is_bit f3)
+       (= (ff.add f0 f1 f2 f3) sum)
+       (= (ff.add d0 (ff.mul #f2m5 d1) (ff.mul #f4m5 d2)) sum)
+       (is_bit d0)
+       (is_bit d1)
+       (is_bit d2))
+  (= (f_to_b d0) (xor (f_to_b f0) (f_to_b f1) (f_to_b f2) (f_to_b f3)))
+)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/ff_xor_unsound_model.smt2 b/test/regress/cli/regress0/ff/ff_xor_unsound_model.smt2
new file mode 100644
index 00000000000..f75654e57a0
--- /dev/null
+++ b/test/regress/cli/regress0/ff/ff_xor_unsound_model.smt2
@@ -0,0 +1,37 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+; XOR compilation strategy (unsound because even though the XOR sum can not
+; overflow, the bit decomposition sum can.
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+(declare-fun f0 () (_ FiniteField 5))
+(declare-fun f1 () (_ FiniteField 5))
+(declare-fun f2 () (_ FiniteField 5))
+(declare-fun f3 () (_ FiniteField 5))
+(declare-fun sum () (_ FiniteField 5))
+(declare-fun d0 () (_ FiniteField 5))
+(declare-fun d1 () (_ FiniteField 5))
+(declare-fun d2 () (_ FiniteField 5))
+(declare-fun b0 () Bool)
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(declare-fun b3 () Bool)
+(define-fun b_to_f ((b Bool)) (_ FiniteField 5) (ite b #f1m5 #f0m5))
+(define-fun f_to_b ((f (_ FiniteField 5))) Bool (not (= f #f0m5)))
+(define-fun is_bit ((f (_ FiniteField 5))) Bool (or (= f #f0m5) (= f #f1m5)))
+(declare-fun m () (_ FiniteField 5))
+(declare-fun is_zero () (_ FiniteField 5))
+(assert (not (=>
+  (and (is_bit f0)
+       (is_bit f1)
+       (is_bit f2)
+       (is_bit f3)
+       (= (ff.add f0 f1 f2 f3) sum)
+       (= (ff.add d0 (ff.mul #f2m5 d1) (ff.mul #f4m5 d2)) sum)
+       (is_bit d0)
+       (is_bit d1)
+       (is_bit d2))
+  (= (f_to_b d0) (xor (f_to_b f0) (f_to_b f1) (f_to_b f2) (f_to_b f3)))
+)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/multicheck.smt2 b/test/regress/cli/regress0/ff/multicheck.smt2
new file mode 100644
index 00000000000..075837f095c
--- /dev/null
+++ b/test/regress/cli/regress0/ff/multicheck.smt2
@@ -0,0 +1,19 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+; EXPECT: sat
+; COMMAND-LINE: --incremental
+; Tests the ff rewriter
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+; all disjuncts should be false
+(define-sort F () (_ FiniteField 17))
+(declare-fun a () F)
+(declare-fun b () F)
+(assert (= (ff.mul a a) b))
+(assert (= a (as ff1 F)))
+(check-sat)
+(declare-fun c () F)
+(assert (= (ff.mul c c) c))
+(assert (= (ff.mul c c) b))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/negneg.smt2 b/test/regress/cli/regress0/ff/negneg.smt2
new file mode 100644
index 00000000000..27435797f72
--- /dev/null
+++ b/test/regress/cli/regress0/ff/negneg.smt2
@@ -0,0 +1,13 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+; x, m, is_zero: field
+; The constraints mx - 1 + is_zero = 0
+;                 is_zero*x = 0
+; Imply that is_zero is zero or one and = (x == 0)
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+(define-sort F () (_ FiniteField 17))
+(declare-fun x () F)
+(assert (not (= (ff.neg (ff.neg x)) x)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/randcompile-sound-3i-5t-circ.smt2 b/test/regress/cli/regress0/ff/randcompile-sound-3i-5t-circ.smt2
new file mode 100644
index 00000000000..fd38f04cd5a
--- /dev/null
+++ b/test/regress/cli/regress0/ff/randcompile-sound-3i-5t-circ.smt2
@@ -0,0 +1,21 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FF)
+
+(declare-const b Bool)
+(declare-const a Bool)
+(declare-const c Bool)
+(declare-const return_n0 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const mul_n7 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const mul_n8 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const mul_n5 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const b_n1 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const mul_n6 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const a_n2 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const mul_n4 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const c_n3 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(assert
+	(not (=> (and (and (= b_n1 (ite b #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (= c_n3 (ite c #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (= a_n2 (ite a #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513))) (and (= (ff.mul b_n1 (ff.add b_n1 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513)) #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513) (= (ff.mul a_n2 (ff.add a_n2 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513)) #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513) (= (ff.mul c_n3 (ff.add c_n3 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513)) #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513) (= (ff.mul a_n2 (ff.add (ff.mul a_n2 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) c_n3)) mul_n4) (= (ff.mul (ff.add mul_n4 a_n2) (ff.add (ff.mul b_n1 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) mul_n5) (= (ff.mul mul_n5 (ff.add (ff.mul mul_n4 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) (ff.mul a_n2 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) mul_n6) (= (ff.mul mul_n6 (ff.add (ff.mul b_n1 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) mul_n7) (= (ff.mul (ff.add (ff.mul mul_n5 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513) (ff.add (ff.mul mul_n7 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) mul_n8) (= (ff.mul mul_n8 (ff.add (ff.mul mul_n7 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) return_n0))) (and (or (= #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 return_n0) (= #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513 return_n0)) (= (= #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 return_n0) (and (=> (ite a c a) b) (or (=> (ite a c a) b) (ite a c a) b) (or (=> (ite a c a) b) (ite a c a) b))))))
+)
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/randcompile-sound-3i-5t-zokcirc.smt2 b/test/regress/cli/regress0/ff/randcompile-sound-3i-5t-zokcirc.smt2
new file mode 100644
index 00000000000..c01a182c528
--- /dev/null
+++ b/test/regress/cli/regress0/ff/randcompile-sound-3i-5t-zokcirc.smt2
@@ -0,0 +1,18 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FF)
+
+(declare-const b Bool)
+(declare-const c Bool)
+(declare-const a Bool)
+(declare-const return_n0 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const mul_n5 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const a_n3 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const b_n1 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const c_n2 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const mul_n4 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(assert
+	(not (=> (and (and (= b_n1 (ite b #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (= c_n2 (ite c #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (= a_n3 (ite a #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513))) (and (= (ff.mul b_n1 (ff.add b_n1 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513)) #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513) (= (ff.mul c_n2 (ff.add c_n2 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513)) #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513) (= (ff.mul a_n3 (ff.add a_n3 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513)) #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513) (= (ff.mul (ff.mul a_n3 #f2m52435875175126190479447740508185965837690552500527637822603658699938581184513) c_n2) mul_n4) (= (ff.mul (ff.add mul_n4 (ff.mul c_n2 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) (ff.mul a_n3 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513) (ff.add (ff.mul b_n1 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) mul_n5) (= (ff.mul a_n3 (ff.add (ff.mul mul_n5 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (ff.add (ff.mul return_n0 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)))) (and (or (= #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 return_n0) (= #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513 return_n0)) (= (= #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 return_n0) (=> a (not (=> (= a c) b)))))))
+)
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/randcompile-sound-3i-5t-zokref.smt2 b/test/regress/cli/regress0/ff/randcompile-sound-3i-5t-zokref.smt2
new file mode 100644
index 00000000000..b2cf988336b
--- /dev/null
+++ b/test/regress/cli/regress0/ff/randcompile-sound-3i-5t-zokref.smt2
@@ -0,0 +1,20 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FF)
+
+(declare-const b Bool)
+(declare-const c Bool)
+(declare-const a Bool)
+(declare-const out (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const _11 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const _10 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const _1 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const _0 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const _6 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const _3 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(declare-const _2 (_ FiniteField 52435875175126190479447740508185965837690552500527637822603658699938581184513))
+(assert
+	(not (=> (and (and (= _1 (ite b #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (= _2 (ite c #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (= _0 (ite a #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513))) (and (= (ff.mul _0 _0) _0) (= (ff.mul _1 _1) _1) (= (ff.mul _2 _2) _2) (= (ff.mul (ff.add (ff.mul _0 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) _1) (ff.add (ff.mul _0 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) _1)) _3) (= (ff.mul (ff.add (ff.mul _3 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513) _2) (ff.add _2 (ff.mul _3 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) (ff.mul _6 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513)) (= (ff.mul _0 _6) _10) (= (ff.mul (ff.add (ff.mul _0 #f52435875175126190479447740508185965837690552500527637822603658699938581184512m52435875175126190479447740508185965837690552500527637822603658699938581184513) #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513) _1) _11) (= (ff.add _10 _11) out))) (and (or (= #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 out) (= #f0m52435875175126190479447740508185965837690552500527637822603658699938581184513 out)) (= (= #f1m52435875175126190479447740508185965837690552500527637822603658699938581184513 out) (ite a (=> (not (= b a)) c) b)))))
+)
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/rewriter.smt2 b/test/regress/cli/regress0/ff/rewriter.smt2
new file mode 100644
index 00000000000..12113e2aa71
--- /dev/null
+++ b/test/regress/cli/regress0/ff/rewriter.smt2
@@ -0,0 +1,33 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+; Tests the ff rewriter
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+; all disjuncts should be false
+(declare-fun x () (_ FiniteField 5))
+(assert (or
+  ; direct !=
+  (= #f2m5 #f1m5 )
+  ; direct ==
+  (not (= #f1m5 #f1m5 ))
+  ; neg: all constants
+  (not (= (ff.neg #f1m5) #f4m5 ))
+  ; add: all constants
+  (not (= (ff.add #f0m5 #f1m5 #f2m5 #f3m5) #f1m5 ))
+  ; add: vars cancel (w/ neg)
+  (not (= (ff.add #f0m5 (ff.neg x) x) #f0m5 ))
+  ; add: vars cancel
+  (not (= (ff.add #f0m5 (ff.mul #f4m5 x) x) #f0m5 ))
+  ; mul: a direct zero
+  (= (ff.mul #f0m5 #f1m5 #f2m5 #f3m5) #f1m5 )
+  ; mul: a direct zero w/ var
+  (= (ff.mul #f0m5 #f1m5 x #f3m5) #f1m5 )
+  ; mul: all constants
+  (not (= (ff.mul #f1m5 #f2m5 #f3m5) #f1m5 ))
+  ; mul: a direct zero w/ var
+  (not (= (ff.mul x #f3m5) (ff.add x x x)))
+  ; mul: a direct zero w/ monomials
+  (not (= (ff.mul x x #f3m5) (ff.add (ff.mul x x) (ff.mul #f2m5 x x))))
+))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/simple.smt2 b/test/regress/cli/regress0/ff/simple.smt2
new file mode 100644
index 00000000000..7d3fe757a38
--- /dev/null
+++ b/test/regress/cli/regress0/ff/simple.smt2
@@ -0,0 +1,20 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+; Tests the ff rewriter
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+; all disjuncts should be false
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert (not (=
+  (or a b c)
+  (not (= (ff.add
+    (ite a #f1m5 #f0m5)
+    (ite b #f1m5 #f0m5)
+    (ite c #f1m5 #f0m5)
+  ) #f0m5
+  ))
+)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/univar_conjunction_sat.smt2 b/test/regress/cli/regress0/ff/univar_conjunction_sat.smt2
new file mode 100644
index 00000000000..8c3b30496e7
--- /dev/null
+++ b/test/regress/cli/regress0/ff/univar_conjunction_sat.smt2
@@ -0,0 +1,12 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+; Tests the ff rewriter
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+; all disjuncts should be false
+(declare-fun x () (_ FiniteField 17))
+(assert (= (ff.mul x x) x))
+(assert (not (= x #f1m17)))
+(assert (not (= x #f2m17)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/univar_conjunction_unsat.smt2 b/test/regress/cli/regress0/ff/univar_conjunction_unsat.smt2
new file mode 100644
index 00000000000..0d7b1abc7d1
--- /dev/null
+++ b/test/regress/cli/regress0/ff/univar_conjunction_unsat.smt2
@@ -0,0 +1,12 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+; Tests the ff rewriter
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+; all disjuncts should be false
+(declare-fun x () (_ FiniteField 17))
+(assert (= (ff.mul x x) x))
+(assert (not (= x #f1m17)))
+(assert (not (= x #f0m17)))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/with_uf.smt2 b/test/regress/cli/regress0/ff/with_uf.smt2
new file mode 100644
index 00000000000..075a012757d
--- /dev/null
+++ b/test/regress/cli/regress0/ff/with_uf.smt2
@@ -0,0 +1,13 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_UFFF)
+(define-sort FF () (_ FiniteField 17))
+(declare-fun f (FF) FF)
+(declare-fun a () FF)
+(declare-fun b () FF)
+(declare-fun c () FF)
+(assert (and (= a b) (= b c) (not (= (f a) (f c)))))
+(check-sat)
+
diff --git a/test/regress/cli/regress0/ff/with_uf2.smt2 b/test/regress/cli/regress0/ff/with_uf2.smt2
new file mode 100644
index 00000000000..7b12a27c888
--- /dev/null
+++ b/test/regress/cli/regress0/ff/with_uf2.smt2
@@ -0,0 +1,18 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_UFFF)
+(define-sort FF () (_ FiniteField 17))
+(declare-fun f (FF) FF)
+(declare-fun a () FF)
+(declare-fun b () FF)
+(declare-fun c () FF)
+(declare-fun e () FF)
+(assert (not (= (f a) (f c))))
+(assert (= b c))
+(assert (= (ff.mul a a) a))
+(assert (= (ff.mul b b) b))
+(assert (= (ff.add (as ff1 FF) (ff.neg a) (ff.neg b) (ff.mul (as ff2 FF) a b)) (as ff1 FF)))
+(check-sat)
+
diff --git a/test/regress/cli/regress0/ff/with_uf3.smt2 b/test/regress/cli/regress0/ff/with_uf3.smt2
new file mode 100644
index 00000000000..8fa59ab49b7
--- /dev/null
+++ b/test/regress/cli/regress0/ff/with_uf3.smt2
@@ -0,0 +1,23 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_UFFF)
+(define-sort FF () (_ FiniteField 17))
+(declare-fun f (FF) FF)
+(declare-fun a () FF)
+(declare-fun b () FF)
+(declare-fun c () FF)
+(assert (not (= (f a) (f c))))
+
+; b = c
+(assert (= (ff.mul c c) c))
+(assert (= (ff.mul b b) b))
+(assert (= (ff.add (as ff1 FF) (ff.neg c) (ff.neg b) (ff.mul (as ff2 FF) c b)) (as ff1 FF)))
+
+; a = b
+(assert (= (ff.mul a a) a))
+(assert (= (ff.mul b b) b))
+(assert (= (ff.add (as ff1 FF) (ff.neg a) (ff.neg b) (ff.mul (as ff2 FF) a b)) (as ff1 FF)))
+(check-sat)
+
diff --git a/test/regress/cli/regress0/ff/with_uf4.smt2 b/test/regress/cli/regress0/ff/with_uf4.smt2
new file mode 100644
index 00000000000..ea45256a59b
--- /dev/null
+++ b/test/regress/cli/regress0/ff/with_uf4.smt2
@@ -0,0 +1,26 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_UFFF)
+(define-sort FF () (_ FiniteField 17))
+(declare-fun f (FF) FF)
+(declare-fun a () FF)
+(declare-fun b () FF)
+(declare-fun c () FF)
+(declare-fun e1 () Bool)
+(declare-fun e2 () Bool)
+(declare-fun e3 () Bool)
+(assert (not (= (f a) (f c))))
+
+; b = c
+(assert (= (ff.mul c c) c))
+(assert (= (ff.mul b b) b))
+(assert (or (= (ff.add (as ff1 FF) (ff.neg c) (ff.neg b) (ff.mul (as ff2 FF) c b)) (as ff1 FF)) (and e1 e2 e3)))
+
+; a = b
+(assert (= (ff.mul a a) a))
+(assert (= (ff.mul b b) b))
+(assert (= (ff.add (as ff1 FF) (ff.neg a) (ff.neg b) (ff.mul (as ff2 FF) a b)) (as ff1 FF)))
+(check-sat)
+
diff --git a/test/regress/cli/regress0/ff/with_uf5.smt2 b/test/regress/cli/regress0/ff/with_uf5.smt2
new file mode 100644
index 00000000000..bc740305898
--- /dev/null
+++ b/test/regress/cli/regress0/ff/with_uf5.smt2
@@ -0,0 +1,23 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_UFFF)
+(define-sort FF () (_ FiniteField 17))
+(declare-fun g (FF) FF)
+(declare-fun a () FF)
+(declare-fun b () FF)
+(declare-fun c () FF)
+(declare-fun d () FF)
+(assert (= a (g c)))
+(assert (= b (g d)))
+
+; c = d
+(assert (= (ff.mul c c) c))
+(assert (= (ff.mul d d) d))
+(assert (= (ff.add (as ff1 FF) (ff.neg c) (ff.neg d) (ff.mul (as ff2 FF) c d)) (as ff1 FF)))
+
+(assert (= a (ff.add b (as ff1 FF))))
+
+(check-sat)
+
diff --git a/test/regress/cli/regress0/ff/with_uf6.smt2 b/test/regress/cli/regress0/ff/with_uf6.smt2
new file mode 100644
index 00000000000..ecc71b44949
--- /dev/null
+++ b/test/regress/cli/regress0/ff/with_uf6.smt2
@@ -0,0 +1,23 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_UFFF)
+(define-sort FF () (_ FiniteField 17))
+(declare-fun g (FF) FF)
+(declare-fun a () FF)
+(declare-fun b () FF)
+(declare-fun c () FF)
+(declare-fun d () FF)
+(assert (= a (g c)))
+(assert (= b (g d)))
+
+; c = d
+(assert (= (ff.mul c c) c))
+(assert (= (ff.mul d d) d))
+(assert (= (ff.add (as ff1 FF) (ff.neg c) (ff.neg d) (ff.mul (as ff2 FF) c d)) (as ff1 FF)))
+
+(assert (= a (ff.add b (as ff0 FF))))
+
+(check-sat)
+
diff --git a/test/regress/cli/regress0/ff/with_uf7.smt2 b/test/regress/cli/regress0/ff/with_uf7.smt2
new file mode 100644
index 00000000000..ae8ff71af3c
--- /dev/null
+++ b/test/regress/cli/regress0/ff/with_uf7.smt2
@@ -0,0 +1,30 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_UFFF)
+(define-sort FF () (_ FiniteField 17))
+(declare-fun g (FF) FF)
+(declare-fun f (FF) FF)
+(declare-fun a () FF)
+(declare-fun b () FF)
+(declare-fun c () FF)
+(declare-fun d () FF)
+(declare-fun e () FF)
+(assert (= a (g c)))
+(assert (= b (g d)))
+
+; c = d
+(assert (= (ff.mul c c) c))
+(assert (= (ff.mul d d) d))
+(assert (= (ff.add (as ff1 FF) (ff.neg c) (ff.neg d) (ff.mul (as ff2 FF) c d)) (as ff1 FF)))
+
+; b = e
+(assert (= (ff.mul b b) b))
+(assert (= (ff.mul e e) e))
+(assert (= (ff.add (as ff1 FF) (ff.neg b) (ff.neg e) (ff.mul (as ff2 FF) b e)) (as ff1 FF)))
+
+(assert (not (= (f a) (f e))))
+
+(check-sat)
+
diff --git a/test/regress/cli/regress0/ff/with_uf8.smt2 b/test/regress/cli/regress0/ff/with_uf8.smt2
new file mode 100644
index 00000000000..3c56243f0e6
--- /dev/null
+++ b/test/regress/cli/regress0/ff/with_uf8.smt2
@@ -0,0 +1,13 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+; COMMAND-LINE: --simplification=none
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_UFFF)
+(define-sort FF () (_ FiniteField 17))
+(declare-fun f (FF) FF)
+(declare-fun d () FF)
+(declare-fun e () FF)
+(assert (and (=  (ff.add d e)  (ff.mul d e)) (=  (ff.mul d e)  (ff.mul e e)) (not (= (f  (ff.add d e)) (f  (ff.mul e e))))))
+(check-sat)
+
diff --git a/test/regress/cli/regress0/ff/with_uf9.smt2 b/test/regress/cli/regress0/ff/with_uf9.smt2
new file mode 100644
index 00000000000..4d62b61f6f7
--- /dev/null
+++ b/test/regress/cli/regress0/ff/with_uf9.smt2
@@ -0,0 +1,10 @@
+; REQUIRES: cocoa
+; EXPECT: unsat
+; COMMAND-LINE: --simplification=none
+(set-logic QF_FF)
+(define-sort FF () (_ FiniteField 17))
+(declare-fun a () FF)
+(declare-fun b () FF)
+(declare-fun c () FF)
+(assert (and (= a b) (= b c) (or (not (= a b)) (not (= a c)))))
+(check-sat)
diff --git a/test/regress/cli/regress0/ff/xor_unsound_missing.smt2 b/test/regress/cli/regress0/ff/xor_unsound_missing.smt2
new file mode 100644
index 00000000000..1082222033e
--- /dev/null
+++ b/test/regress/cli/regress0/ff/xor_unsound_missing.smt2
@@ -0,0 +1,38 @@
+; REQUIRES: cocoa
+; EXPECT: sat
+; XOR compilation strategy
+; unsound because of a missing bit-constraint.
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+(declare-fun f0 () (_ FiniteField 11))
+(declare-fun f1 () (_ FiniteField 11))
+(declare-fun f2 () (_ FiniteField 11))
+(declare-fun f3 () (_ FiniteField 11))
+(declare-fun sum () (_ FiniteField 11))
+(declare-fun d0 () (_ FiniteField 11))
+(declare-fun d1 () (_ FiniteField 11))
+(declare-fun d2 () (_ FiniteField 11))
+(declare-fun b0 () Bool)
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(declare-fun b3 () Bool)
+(define-fun b_to_f ((b Bool)) (_ FiniteField 11) (ite b #f1m11 #f0m11))
+(define-fun f_to_b ((f (_ FiniteField 11))) Bool (not (= f #f0m11)))
+(define-fun is_bit ((f (_ FiniteField 11))) Bool (or (= f #f0m11) (= f #f1m11)))
+(declare-fun m () (_ FiniteField 11))
+(declare-fun is_zero () (_ FiniteField 11))
+(assert (not (=>
+  (and (is_bit f0)
+       (is_bit f1)
+       (is_bit f2)
+       (is_bit f3)
+       (= (ff.add f0 f1 f2 f3) sum)
+       (= (ff.add d0 (ff.mul #f2m11 d1) (ff.mul #f4m11 d2)) sum)
+       (is_bit d0)
+       (is_bit d1)
+       ; (is_bit d2) this is missing
+       )
+  (= (f_to_b d0) (xor (f_to_b f0) (f_to_b f1) (f_to_b f2) (f_to_b f3)))
+)))
+(check-sat)
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 7341456118b..982163fc268 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -186,6 +186,12 @@ TEST_F(TestApiBlackSolver, mkBitVectorSort)
   ASSERT_THROW(d_solver.mkBitVectorSort(0), CVC5ApiException);
 }
 
+TEST_F(TestApiBlackSolver, mkFiniteFieldSort)
+{
+  ASSERT_NO_THROW(d_solver.mkFiniteFieldSort("31"));
+  ASSERT_THROW(d_solver.mkFiniteFieldSort("6"), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackSolver, mkFloatingPointSort)
 {
   ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8));
@@ -466,6 +472,25 @@ TEST_F(TestApiBlackSolver, mkBitVector)
             d_solver.mkBitVector(8, "FF", 16));
 }
 
+TEST_F(TestApiBlackSolver, mkFiniteFieldElem)
+{
+  Sort f = d_solver.mkFiniteFieldSort("7");
+  Sort bv = d_solver.mkBitVectorSort(4);
+
+  ASSERT_NO_THROW(d_solver.mkFiniteFieldElem("0", f));
+  ASSERT_NO_THROW(d_solver.mkFiniteFieldElem("1", f));
+  ASSERT_NO_THROW(d_solver.mkFiniteFieldElem("6", f));
+  ASSERT_NO_THROW(d_solver.mkFiniteFieldElem("8", f));
+  ASSERT_NO_THROW(d_solver.mkFiniteFieldElem("-1", f));
+
+  ASSERT_THROW(d_solver.mkFiniteFieldElem("-1", bv), CVC5ApiException);
+
+  ASSERT_EQ(d_solver.mkFiniteFieldElem("-1", f),
+            d_solver.mkFiniteFieldElem("6", f));
+  ASSERT_EQ(d_solver.mkFiniteFieldElem("1", f),
+            d_solver.mkFiniteFieldElem("8", f));
+}
+
 TEST_F(TestApiBlackSolver, mkVar)
 {
   Sort boolSort = d_solver.getBooleanSort();
diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp
index 7070c6acc49..7db032d7799 100644
--- a/test/unit/api/cpp/sort_black.cpp
+++ b/test/unit/api/cpp/sort_black.cpp
@@ -135,6 +135,12 @@ TEST_F(TestApiBlackSort, isBitVector)
   ASSERT_NO_THROW(Sort().isBitVector());
 }
 
+TEST_F(TestApiBlackSort, isFiniteField)
+{
+  ASSERT_TRUE(d_solver.mkFiniteFieldSort("7").isFiniteField());
+  ASSERT_NO_THROW(Sort().isFiniteField());
+}
+
 TEST_F(TestApiBlackSort, isFloatingPoint)
 {
   ASSERT_TRUE(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint());
@@ -518,6 +524,16 @@ TEST_F(TestApiBlackSort, getBitVectorSize)
   ASSERT_THROW(setSort.getBitVectorSize(), CVC5ApiException);
 }
 
+TEST_F(TestApiBlackSort, getFiniteFieldSize)
+{
+  Sort ffSort = d_solver.mkFiniteFieldSort("31");
+  ASSERT_NO_THROW(ffSort.getFiniteFieldSize());
+  ASSERT_EQ(ffSort.getFiniteFieldSize(), "31");
+  ASSERT_THROW(Sort().getFiniteFieldSize(), CVC5ApiException);
+  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+  ASSERT_THROW(setSort.getFiniteFieldSize(), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackSort, getFloatingPointExponentSize)
 {
   Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp
index 46247e0337b..b4be2db90a8 100644
--- a/test/unit/api/cpp/term_black.cpp
+++ b/test/unit/api/cpp/term_black.cpp
@@ -915,6 +915,25 @@ TEST_F(TestApiBlackTerm, getBitVector)
   ASSERT_EQ("f", b7.getBitVectorValue(16));
 }
 
+TEST_F(TestApiBlackTerm, isFiniteFieldValue)
+{
+  Sort fS = d_solver.mkFiniteFieldSort("7");
+  Term fV = d_solver.mkFiniteFieldElem("1", fS);
+  ASSERT_TRUE(fV.isFiniteFieldValue());
+  Term b1 = d_solver.mkBitVector(8, 15);
+  ASSERT_FALSE(b1.isFiniteFieldValue());
+}
+
+TEST_F(TestApiBlackTerm, getFiniteFieldValue)
+{
+  Sort fS = d_solver.mkFiniteFieldSort("7");
+  Term fV = d_solver.mkFiniteFieldElem("1", fS);
+  ASSERT_EQ("1", fV.getFiniteFieldValue());
+  ASSERT_THROW(Term().getFiniteFieldValue(), CVC5ApiException);
+  Term b1 = d_solver.mkBitVector(8, 15);
+  ASSERT_THROW(b1.getFiniteFieldValue(), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackTerm, getUninterpretedSortValue)
 {
   d_solver.setOption("produce-models", "true");
diff --git a/test/unit/node/type_cardinality_black.cpp b/test/unit/node/type_cardinality_black.cpp
index 21b97ea3d8d..eca76e7f38a 100644
--- a/test/unit/node/type_cardinality_black.cpp
+++ b/test/unit/node/type_cardinality_black.cpp
@@ -345,8 +345,8 @@ TEST_F(TestNodeBlackTypeCardinality, lessThan)
   ASSERT_FALSE(d_nodeManager->roundingModeType().isCardinalityLessThan(5));
   ASSERT_TRUE(d_nodeManager->roundingModeType().isCardinalityLessThan(6));
   ASSERT_FALSE(
-      d_nodeManager->mkFiniteFieldType(256).isCardinalityLessThan(256));
-  ASSERT_TRUE(d_nodeManager->mkFiniteFieldType(256).isCardinalityLessThan(257));
+      d_nodeManager->mkFiniteFieldType(11).isCardinalityLessThan(11));
+  ASSERT_TRUE(d_nodeManager->mkFiniteFieldType(11).isCardinalityLessThan(13));
 }
 }  // namespace test
 }  // namespace cvc5::internal