diff --git a/src/theory/ff/cocoa_encoder.cpp b/src/theory/ff/cocoa_encoder.cpp
index a2540e7edac..abf5ff17942 100644
--- a/src/theory/ff/cocoa_encoder.cpp
+++ b/src/theory/ff/cocoa_encoder.cpp
@@ -214,6 +214,16 @@ FiniteFieldValue CocoaEncoder::cocoaFfToFfVal(const Scalar& elem)
   return ff::cocoaFfToFfVal(elem, size());
 }
 
+const Node& CocoaEncoder::polyFact(const Poly& poly) const
+{
+  return d_polyFacts.at(extractStr(poly));
+}
+
+bool CocoaEncoder::polyHasFact(const Poly& poly) const
+{
+  return d_polyFacts.count(extractStr(poly));
+}
+
 const Poly& CocoaEncoder::symPoly(CoCoA::symbol s) const
 {
   Assert(d_symPolys.count(extractStr(s)));
@@ -293,12 +303,13 @@ void CocoaEncoder::encodeFact(const Node& f)
 {
   Assert(d_stage == Stage::Encode);
   Assert(isFfFact(f, size()));
+  Poly p;
   // ==
   if (f.getKind() == Kind::EQUAL)
   {
     encodeTerm(f[0]);
     encodeTerm(f[1]);
-    d_cache.insert({f, d_cache.at(f[0]) - d_cache.at(f[1])});
+    p = d_cache.at(f[0]) - d_cache.at(f[1]);
   }
   // !=
   else
@@ -306,8 +317,10 @@ void CocoaEncoder::encodeFact(const Node& f)
     encodeTerm(f[0][0]);
     encodeTerm(f[0][1]);
     Poly diff = d_cache.at(f[0][0]) - d_cache.at(f[0][1]);
-    d_cache.insert({f, diff * symPoly(d_diseqSyms.at(f)) - 1});
+    p = diff * symPoly(d_diseqSyms.at(f)) - 1;
   }
+  d_cache.insert({f, p});
+  d_polyFacts.insert({extractStr(p), f});
 }
 
 }  // namespace ff
diff --git a/src/theory/ff/cocoa_encoder.h b/src/theory/ff/cocoa_encoder.h
index 42b270f5bdb..52352b63afe 100644
--- a/src/theory/ff/cocoa_encoder.h
+++ b/src/theory/ff/cocoa_encoder.h
@@ -33,6 +33,7 @@
 // internal includes
 #include "expr/node.h"
 #include "theory/ff/cocoa_util.h"
+#include "theory/ff/core.h"
 #include "theory/ff/util.h"
 
 namespace cvc5::internal {
@@ -103,6 +104,14 @@ class CocoaEncoder : public FieldObj
    * Convert a (coefficient) Scalar to a FiniteFieldValue.
    */
   FiniteFieldValue cocoaFfToFfVal(const Scalar& elem);
+  /**
+   * Does some fact that imply this poly?
+   */
+  bool polyHasFact(const Poly& poly) const;
+  /**
+   * Get the fact that implies this poly.
+   */
+  const Node& polyFact(const Poly& poly) const;
 
  private:
   /**
@@ -168,6 +177,8 @@ class CocoaEncoder : public FieldObj
   std::vector<Poly> d_polys{};
   /** bitsum polynomials that must be zero */
   std::vector<Poly> d_bitsumPolys{};
+  /** polys to the facts that imply them */
+  std::unordered_map<std::string, Node> d_polyFacts{};
 };
 
 }  // namespace ff
diff --git a/src/theory/ff/cocoa_util.cpp b/src/theory/ff/cocoa_util.cpp
index d7b72e9f99e..d557c2ffebe 100644
--- a/src/theory/ff/cocoa_util.cpp
+++ b/src/theory/ff/cocoa_util.cpp
@@ -21,6 +21,8 @@
 #include <CoCoA/BigIntOps.H>
 #include <CoCoA/SparsePolyIter.H>
 #include <CoCoA/SparsePolyOps-RingElem.H>
+#include <CoCoA/SparsePolyOps-ideal.H>
+#include <CoCoA/TmpGPoly.H>
 
 // std includes
 
@@ -88,6 +90,33 @@ CoCoA::BigInt intToCocoa(const Integer& i)
   return CoCoA::BigIntFromString(i.toString());
 }
 
+const std::vector<Poly>& GBasisTimeout(const CoCoA::ideal& ideal,
+                                       const ResourceManager* rm)
+{
+  if (rm == nullptr)
+  {
+    return CoCoA::GBasis(ideal);
+  }
+  double sec = static_cast<double>(rm->getRemainingTime()) / 1e3;
+  Trace("ff::gb") << "Computing a GB; limit " << sec << "s" << std::endl;
+  try
+  {
+    if (sec == 0)
+    {
+      return CoCoA::GBasis(ideal);
+    }
+    else
+    {
+      return CoCoA::GBasis(ideal, CoCoA::CpuTimeLimit(sec));
+    }
+  }
+  catch (CoCoA::TimeoutException& t)
+  {
+    CoCoA::handlersEnabled = false;
+    throw FfTimeoutException("GBasis");
+  }
+}
+
 }  // namespace ff
 }  // namespace theory
 }  // namespace cvc5::internal
diff --git a/src/theory/ff/cocoa_util.h b/src/theory/ff/cocoa_util.h
index 47db7096238..6f1a7d67d07 100644
--- a/src/theory/ff/cocoa_util.h
+++ b/src/theory/ff/cocoa_util.h
@@ -30,8 +30,10 @@
 #include <vector>
 
 // internal includes
+#include "theory/ff/util.h"
 #include "util/finite_field_value.h"
 #include "util/integer.h"
+#include "util/resource_manager.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -76,6 +78,13 @@ std::string extractStr(const T& t)
   return o.str();
 }
 
+/**
+ * Compute a GB, with timeout given by `rm`.
+ * Throws an FfTimeoutException if the timeout is exceeded.
+ */
+const std::vector<Poly>& GBasisTimeout(const CoCoA::ideal& ideal,
+                                       const ResourceManager* rm);
+
 }  // namespace ff
 }  // namespace theory
 }  // namespace cvc5::internal
diff --git a/src/theory/ff/multi_roots.cpp b/src/theory/ff/multi_roots.cpp
index 2dbf75dd150..19cd9622371 100644
--- a/src/theory/ff/multi_roots.cpp
+++ b/src/theory/ff/multi_roots.cpp
@@ -30,7 +30,10 @@
 #include <sstream>
 
 #include "smt/assertions.h"
+#include "theory/ff/cocoa_util.h"
 #include "theory/ff/uni_roots.h"
+#include "theory/ff/util.h"
+#include "util/resource_manager.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -135,6 +138,7 @@ std::pair<size_t, CoCoA::RingElem> extractAssignment(
 std::unordered_set<std::string> assignedVars(const CoCoA::ideal& ideal)
 {
   std::unordered_set<std::string> ret{};
+  Assert(CoCoA::HasGBasis(ideal));
   for (const auto& g : CoCoA::GBasis(ideal))
   {
     if (CoCoA::deg(g) == 1)
@@ -160,6 +164,7 @@ std::unique_ptr<AssignmentEnumerator> applyRule(const CoCoA::ideal& ideal)
   CoCoA::ring polyRing = ideal->myRing();
   Assert(!isUnsat(ideal));
   // first, we look for super-linear univariate polynomials.
+  Assert(CoCoA::HasGBasis(ideal));
   const auto& gens = CoCoA::GBasis(ideal);
   for (const auto& p : gens)
   {
@@ -208,7 +213,8 @@ std::unique_ptr<AssignmentEnumerator> applyRule(const CoCoA::ideal& ideal)
   }
 }
 
-std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& initialIdeal)
+std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& initialIdeal,
+                                      const Env& env)
 {
   CoCoA::ring polyRing = initialIdeal->myRing();
   // We maintain two stacks:
@@ -242,8 +248,16 @@ std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& initialIdeal)
   // while some ideal might have a zero.
   while (!ideals.empty())
   {
-    // choose one
+    // check for timeout
+    if (env.getResourceManager()->outOfTime())
+    {
+      throw FfTimeoutException("findZero");
+    }
+    // choose one ideal
     const auto& ideal = ideals.back();
+    // make sure we have a GBasis:
+    GBasisTimeout(ideal, env.getResourceManager());
+    Assert(CoCoA::HasGBasis(ideal));
     // If the ideal is UNSAT, drop it.
     if (isUnsat(ideal))
     {
@@ -254,6 +268,7 @@ std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& initialIdeal)
     else if (allVarsAssigned(ideal))
     {
       std::unordered_map<size_t, CoCoA::RingElem> varNumToValue{};
+      Assert(CoCoA::HasGBasis(ideal));
       const auto& gens = CoCoA::GBasis(ideal);
       size_t numIndets = CoCoA::NumIndets(polyRing);
       Assert(gens.size() == numIndets);
@@ -296,6 +311,7 @@ std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& initialIdeal)
             << "level: " << branchers.size()
             << ", brancher: " << branchers.back()->name()
             << ", branch: " << choicePoly.value() << std::endl;
+        Assert(CoCoA::HasGBasis(ideal));
         std::vector<CoCoA::RingElem> newGens = CoCoA::GBasis(ideal);
         newGens.push_back(choicePoly.value());
         ideals.push_back(CoCoA::ideal(newGens));
diff --git a/src/theory/ff/multi_roots.h b/src/theory/ff/multi_roots.h
index 8f50227f3f9..b0116c354cc 100644
--- a/src/theory/ff/multi_roots.h
+++ b/src/theory/ff/multi_roots.h
@@ -32,6 +32,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/env.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -40,7 +41,7 @@ namespace ff {
 /**
  * Find a common zero for all poynomials in this ideal. Figure 5 from [OKTB23].
  */
-std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& ideal);
+std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& ideal, const Env& env);
 
 /**
  * Enumerates **assignment**s: monic, degree-one, univariate polynomials.
diff --git a/src/theory/ff/split_gb.cpp b/src/theory/ff/split_gb.cpp
index 4f63043f3e3..ab3e3d15aee 100644
--- a/src/theory/ff/split_gb.cpp
+++ b/src/theory/ff/split_gb.cpp
@@ -31,13 +31,14 @@
 // internal includes
 #include "base/output.h"
 #include "theory/ff/parse.h"
+#include "util/resource_manager.h"
 
 namespace cvc5::internal {
 namespace theory {
 namespace ff {
 
 std::optional<std::unordered_map<Node, FiniteFieldValue>> split(
-    const std::vector<Node>& facts, const FfSize& size)
+    const std::vector<Node>& facts, const FfSize& size, const Env& env)
 {
   std::unordered_set<Node> bits{};
   CocoaEncoder enc(size);
@@ -64,7 +65,7 @@ std::optional<std::unordered_map<Node, FiniteFieldValue>> split(
   BitProp bitProp(facts, enc);
 
   std::vector<Polys> splitGens = {lGens, nlGens};
-  SplitGb splitBasis = splitGb(splitGens, bitProp);
+  SplitGb splitBasis = splitGb(splitGens, bitProp, env);
   if (std::any_of(splitBasis.begin(), splitBasis.end(), [](const auto& b) {
         return b.isWholeRing();
       }))
@@ -73,7 +74,7 @@ std::optional<std::unordered_map<Node, FiniteFieldValue>> split(
   }
 
   std::optional<Point> root =
-      splitFindZero(std::move(splitBasis), enc.polyRing(), bitProp);
+      splitFindZero(std::move(splitBasis), enc.polyRing(), bitProp, env);
   if (root.has_value())
   {
     std::unordered_map<Node, FiniteFieldValue> model;
@@ -89,7 +90,9 @@ std::optional<std::unordered_map<Node, FiniteFieldValue>> split(
   return {};
 }
 
-SplitGb splitGb(const std::vector<Polys>& generatorSets, BitProp& bitProp)
+SplitGb splitGb(const std::vector<Polys>& generatorSets,
+                BitProp& bitProp,
+                const Env& env)
 {
   size_t k = generatorSets.size();
   std::vector<Polys> newPolys(generatorSets);
@@ -108,7 +111,7 @@ SplitGb splitGb(const std::vector<Polys>& generatorSets, BitProp& bitProp)
         std::copy(newPolys[i].begin(),
                   newPolys[i].end(),
                   std::back_inserter(newGens));
-        splitBasis[i] = Gb(newGens);
+        splitBasis[i] = Gb(newGens, env.getResourceManager());
         newPolys[i].clear();
       }
     }
@@ -146,7 +149,8 @@ bool admit(size_t i, const Poly& p)
 
 std::optional<Point> splitFindZero(SplitGb&& splitBasisIn,
                                    CoCoA::ring polyRing,
-                                   BitProp& bitProp)
+                                   BitProp& bitProp,
+                                   const Env& env)
 {
   SplitGb splitBasis = std::move(splitBasisIn);
   while (true)
@@ -159,7 +163,7 @@ std::optional<Point> splitFindZero(SplitGb&& splitBasisIn,
     }
     PartialPoint nullPartialRoot(CoCoA::NumIndets(polyRing));
     auto result = splitZeroExtend(
-        allGens, SplitGb(splitBasis), std::move(nullPartialRoot), bitProp);
+        allGens, SplitGb(splitBasis), std::move(nullPartialRoot), bitProp, env);
     if (std::holds_alternative<Poly>(result))
     {
       auto conflict = std::get<Poly>(result);
@@ -172,7 +176,7 @@ std::optional<Point> splitFindZero(SplitGb&& splitBasisIn,
                   std::back_inserter(gens.back()));
         gens.back().push_back(conflict);
       }
-      splitBasis = splitGb(gens, bitProp);
+      splitBasis = splitGb(gens, bitProp, env);
     }
     else if (std::holds_alternative<bool>(result))
     {
@@ -188,7 +192,8 @@ std::optional<Point> splitFindZero(SplitGb&& splitBasisIn,
 std::variant<Point, Poly, bool> splitZeroExtend(const Polys& origPolys,
                                                 const SplitGb&& curBases,
                                                 const PartialPoint&& curR,
-                                                const BitProp& bitProp)
+                                                const BitProp& bitProp,
+                                                const Env& env)
 {
   Assert(origPolys.size());
   CoCoA::ring polyRing = CoCoA::owner(origPolys[0]);
@@ -211,6 +216,11 @@ std::variant<Point, Poly, bool> splitZeroExtend(const Polys& origPolys,
     return false;
   }
 
+  if (env.getResourceManager()->outOfTime())
+  {
+    throw FfTimeoutException("splitZeroExtend");
+  }
+
   if (nAssigned == CoCoA::NumIndets(CoCoA::owner(origPolys[0])))
   {
     Point out;
@@ -242,9 +252,9 @@ std::variant<Point, Poly, bool> splitZeroExtend(const Polys& origPolys,
       newSplitGens.back().push_back(*next);
     }
     BitProp bitPropCopy = bitProp;
-    SplitGb newBases = splitGb(newSplitGens, bitPropCopy);
+    SplitGb newBases = splitGb(newSplitGens, bitPropCopy, env);
     auto result = splitZeroExtend(
-        origPolys, std::move(newBases), std::move(newR), bitPropCopy);
+        origPolys, std::move(newBases), std::move(newR), bitPropCopy, env);
     if (!std::holds_alternative<bool>(result))
     {
       return result;
@@ -333,12 +343,13 @@ void checkZero(const SplitGb& origBases, const Point& zero)
 }
 
 Gb::Gb() : d_ideal(), d_basis(){};
-Gb::Gb(const Polys& generators) : d_ideal(), d_basis()
+Gb::Gb(const std::vector<Poly>& generators, const ResourceManager* rm)
+    : d_ideal(), d_basis()
 {
   if (generators.size())
   {
     d_ideal.emplace(CoCoA::ideal(generators));
-    d_basis = CoCoA::GBasis(d_ideal.value());
+    d_basis = GBasisTimeout(d_ideal.value(), rm);
   }
 }
 
diff --git a/src/theory/ff/split_gb.h b/src/theory/ff/split_gb.h
index 3045468844f..8abef0a1001 100644
--- a/src/theory/ff/split_gb.h
+++ b/src/theory/ff/split_gb.h
@@ -48,6 +48,7 @@
 #include "theory/ff/cocoa_encoder.h"
 #include "theory/ff/cocoa_util.h"
 #include "theory/ff/multi_roots.h"
+#include "util/resource_manager.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -65,22 +66,26 @@ using SplitGb = std::vector<Gb>;
  *
  * @param facts Finite field equalities and disequalities.
  * @param size The size of the field they are in.
+ * @param env used for resource management
  *
  * @return A model, or not if none exists.
  * */
 std::optional<FfModel> split(const std::vector<Node>& facts,
-                             const FfSize& size);
+                             const FfSize& size,
+                             const Env& env);
 
 /** Compute a split Gb.
  *
  * @param generatorSets A collection of collections of polynomials.
  * @param bitProp A data structure that stores information about which CoCoA
  *                variables are bitsums of which other CoCoA variables.
+ * @param env used for resource management
  *
  * @return A split Groebner basis for the ideal generated by generatorSets.
  * */
 std::vector<Gb> splitGb(const std::vector<std::vector<Poly>>& generatorSets,
-                        BitProp& bitProp);
+                        BitProp& bitProp,
+                        const Env& env);
 
 /** Whether to admit p into ideal i. */
 bool admit(size_t i, const Poly& p);
@@ -90,6 +95,7 @@ bool admit(size_t i, const Poly& p);
  * @param splitBasis A split Groebner basis.
  * @param polyRing The polynomial ring it's in.
  * @param bitProp Info about which vars are bitsums of which. See splitGb.
+ * @param env used for resource management
  *
  * @return A common zero for all polynomials in the ideal generated by
  *         splitBasis, or not if none exists.
@@ -97,7 +103,8 @@ bool admit(size_t i, const Poly& p);
  * */
 std::optional<Point> splitFindZero(SplitGb&& splitBasis,
                                    CoCoA::ring polyRing,
-                                   BitProp& bitProp);
+                                   BitProp& bitProp,
+                                   const Env& env);
 
 /** Extend curR into a zero for this split Gb.
  *
@@ -105,6 +112,7 @@ std::optional<Point> splitFindZero(SplitGb&& splitBasis,
  * @param curBases A split basis for the same ideal.
  * @param curR A partial zero for the ideal.
  * @param bitProp Info about which vars are bitsums of which. See splitGb.
+ * @param env used for resource management
  *
  * @return A common (full) zero, a conflict polynomial, or false (indicating
  *         that no common zeros exist). The conflict polynomial is guaranteed to
@@ -114,7 +122,8 @@ std::variant<Point, Poly, bool> splitZeroExtend(
     const std::vector<Poly>& origPolys,
     const SplitGb&& curBases,
     const PartialPoint&& curR,
-    const BitProp& bitProp);
+    const BitProp& bitProp,
+    const Env& env);
 
 /** Apply a branching rule.
  *
@@ -138,7 +147,7 @@ class Gb
  public:
   Gb();
   /** A GB for the ideal generated by generators */
-  Gb(const std::vector<Poly>& generators);
+  Gb(const std::vector<Poly>& generators, const ResourceManager* rm);
   /** Does this GB's ideal contain p? */
   bool contains(const Poly& p) const;
   /** Is this GB's ideal equal to the whole ring? */
diff --git a/src/theory/ff/sub_theory.cpp b/src/theory/ff/sub_theory.cpp
index 626a2c9496b..741aac7bdee 100644
--- a/src/theory/ff/sub_theory.cpp
+++ b/src/theory/ff/sub_theory.cpp
@@ -22,6 +22,7 @@
 #include "theory/ff/sub_theory.h"
 
 #include <CoCoA/BigInt.H>
+#include <CoCoA/CpuTimeLimit.H>
 #include <CoCoA/QuotientRing.H>
 #include <CoCoA/RingZZ.H>
 #include <CoCoA/SparsePolyOps-ideal.H>
@@ -36,8 +37,10 @@
 #include "theory/ff/core.h"
 #include "theory/ff/multi_roots.h"
 #include "theory/ff/split_gb.h"
+#include "theory/ff/util.h"
 #include "util/cocoa_globals.h"
 #include "util/finite_field_value.h"
+#include "util/resource_manager.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -59,122 +62,138 @@ Result SubTheory::postCheck(Theory::Effort e)
   d_model.clear();
   if (e == Theory::EFFORT_FULL)
   {
-    if (d_facts.empty()) return Result::SAT;
-    if (options().ff.ffSolver == options::FfSolver::SPLIT_GB)
+    try
     {
-      std::vector<Node> facts{};
-      std::copy(d_facts.begin(), d_facts.end(), std::back_inserter(facts));
-      auto result = split(facts, size());
-      if (result.has_value())
+      if (d_facts.empty()) return Result::SAT;
+      if (options().ff.ffSolver == options::FfSolver::SPLIT_GB)
       {
-        const auto nm = nodeManager();
-        for (const auto& [var, val] : result.value())
+        std::vector<Node> facts{};
+        std::copy(d_facts.begin(), d_facts.end(), std::back_inserter(facts));
+        auto result = split(facts, size(), d_env);
+        if (result.has_value())
         {
-          d_model.insert({var, nm->mkConst<FiniteFieldValue>(val)});
+          const auto nm = nodeManager();
+          for (const auto& [var, val] : result.value())
+          {
+            d_model.insert({var, nm->mkConst<FiniteFieldValue>(val)});
+          }
+          return Result::SAT;
         }
-        return Result::SAT;
+        std::copy(
+            d_facts.begin(), d_facts.end(), std::back_inserter(d_conflict));
+        return Result::UNSAT;
       }
-      std::copy(d_facts.begin(), d_facts.end(), std::back_inserter(d_conflict));
-      return Result::UNSAT;
-    }
-    else if (options().ff.ffSolver == options::FfSolver::GB)
-    {
-      CocoaEncoder enc(size());
-      // collect leaves
-      for (const Node& node : d_facts)
+      else if (options().ff.ffSolver == options::FfSolver::GB)
       {
-        enc.addFact(node);
-      }
-      enc.endScan();
-      // assert facts
-      for (const Node& node : d_facts)
-      {
-        enc.addFact(node);
-      }
+        CocoaEncoder enc(size());
+        // collect leaves
+        for (const Node& node : d_facts)
+        {
+          enc.addFact(node);
+        }
+        enc.endScan();
+        // assert facts
+        for (const Node& node : d_facts)
+        {
+          enc.addFact(node);
+        }
 
-      // compute a GB
-      std::vector<CoCoA::RingElem> generators;
-      generators.insert(
-          generators.end(), enc.polys().begin(), enc.polys().end());
-      generators.insert(
-          generators.end(), enc.bitsumPolys().begin(), enc.bitsumPolys().end());
-      size_t nNonFieldPolyGens = generators.size();
-      if (options().ff.ffFieldPolys)
-      {
-        for (const auto& var : CoCoA::indets(enc.polyRing()))
+        // compute a GB
+        std::vector<CoCoA::RingElem> generators;
+        generators.insert(
+            generators.end(), enc.polys().begin(), enc.polys().end());
+        generators.insert(generators.end(),
+                          enc.bitsumPolys().begin(),
+                          enc.bitsumPolys().end());
+        if (options().ff.ffFieldPolys)
         {
-          CoCoA::BigInt characteristic = CoCoA::characteristic(coeffRing());
-          long power = CoCoA::LogCardinality(coeffRing());
-          CoCoA::BigInt size = CoCoA::power(characteristic, power);
-          generators.push_back(CoCoA::power(var, size) - var);
+          for (const auto& var : CoCoA::indets(enc.polyRing()))
+          {
+            CoCoA::BigInt characteristic = CoCoA::characteristic(coeffRing());
+            long power = CoCoA::LogCardinality(coeffRing());
+            CoCoA::BigInt size = CoCoA::power(characteristic, power);
+            generators.push_back(CoCoA::power(var, size) - var);
+          }
         }
-      }
-      Tracer tracer(generators);
-      if (options().ff.ffTraceGb) tracer.setFunctionPointers();
-      CoCoA::ideal ideal = CoCoA::ideal(generators);
-      const auto basis = CoCoA::GBasis(ideal);
-      if (options().ff.ffTraceGb) tracer.unsetFunctionPointers();
-
-      // if it is trivial, create a conflict
-      bool is_trivial = basis.size() == 1 && CoCoA::deg(basis.front()) == 0;
-      if (is_trivial)
-      {
-        Trace("ff::gb") << "Trivial GB" << std::endl;
-        if (options().ff.ffTraceGb)
+        Tracer tracer(generators);
+        if (options().ff.ffTraceGb) tracer.setFunctionPointers();
+        CoCoA::ideal ideal = CoCoA::ideal(generators);
+        const auto basis = GBasisTimeout(ideal, d_env.getResourceManager());
+        if (options().ff.ffTraceGb) tracer.unsetFunctionPointers();
+
+        // if it is trivial, create a conflict
+        bool is_trivial = basis.size() == 1 && CoCoA::deg(basis.front()) == 0;
+        if (is_trivial)
         {
-          std::vector<size_t> coreIndices = tracer.trace(basis.front());
-          Assert(d_conflict.empty());
-          for (size_t i : coreIndices)
+          Trace("ff::gb") << "Trivial GB" << std::endl;
+          if (options().ff.ffTraceGb)
           {
-            // omit field polys from core
-            if (i < nNonFieldPolyGens)
+            std::vector<size_t> coreIndices = tracer.trace(basis.front());
+            Assert(d_conflict.empty());
+            for (size_t i = 0, n = d_facts.size(); i < n; ++i)
             {
-              Trace("ff::core") << "Core: " << d_facts[i] << std::endl;
-              d_conflict.push_back(d_facts[i]);
+              Trace("ff::core")
+                  << "In " << i << " : " << d_facts[i] << std::endl;
             }
+            for (size_t i : coreIndices)
+            {
+              // omit (field polys, bitsum polys, ...) from core
+              if (enc.polyHasFact(generators[i]))
+              {
+                Trace("ff::core")
+                    << "Core: " << i << " : " << d_facts[i] << std::endl;
+                d_conflict.push_back(enc.polyFact(generators[i]));
+              }
+            }
+          }
+          else
+          {
+            setTrivialConflict();
           }
         }
         else
         {
-          setTrivialConflict();
-        }
-      }
-      else
-      {
-        Trace("ff::gb") << "Non-trivial GB" << std::endl;
+          Trace("ff::gb") << "Non-trivial GB" << std::endl;
 
-        // common root (vec of CoCoA base ring elements)
-        std::vector<CoCoA::RingElem> root = findZero(ideal);
+          // common root (vec of CoCoA base ring elements)
+          std::vector<CoCoA::RingElem> root = findZero(ideal, d_env);
 
-        if (root.empty())
-        {
-          // UNSAT
-          setTrivialConflict();
-        }
-        else
-        {
-          // SAT: populate d_model from the root
-          Assert(d_model.empty());
-          const auto nm = nodeManager();
-          Trace("ff::model") << "Model GF(" << size() << "):" << std::endl;
-          for (const auto& [idx, node] : enc.nodeIndets())
+          if (root.empty())
+          {
+            // UNSAT
+            setTrivialConflict();
+          }
+          else
           {
-            if (isFfLeaf(node))
+            // SAT: populate d_model from the root
+            Assert(d_model.empty());
+            const auto nm = nodeManager();
+            Trace("ff::model") << "Model GF(" << size() << "):" << std::endl;
+            for (const auto& [idx, node] : enc.nodeIndets())
             {
-              Node value = nm->mkConst(enc.cocoaFfToFfVal(root[idx]));
-              Trace("ff::model") << " " << node << " = " << value << std::endl;
-              d_model.emplace(node, value);
+              if (isFfLeaf(node))
+              {
+                Node value = nm->mkConst(enc.cocoaFfToFfVal(root[idx]));
+                Trace("ff::model")
+                    << " " << node << " = " << value << std::endl;
+                d_model.emplace(node, value);
+              }
             }
           }
         }
       }
+      else
+      {
+        Unreachable() << options().ff.ffSolver << std::endl;
+      }
+      AlwaysAssert((!d_conflict.empty() ^ !d_model.empty()) || d_facts.empty());
+      return d_facts.empty() || d_conflict.empty() ? Result::SAT
+                                                   : Result::UNSAT;
     }
-    else
+    catch (FfTimeoutException& exc)
     {
-      Unreachable() << options().ff.ffSolver << std::endl;
+      return {Result::UNKNOWN, UnknownExplanation::TIMEOUT, exc.getMessage()};
     }
-    AlwaysAssert((!d_conflict.empty() ^ !d_model.empty()) || d_facts.empty());
-    return d_facts.empty() || d_conflict.empty() ? Result::SAT : Result::UNSAT;
   }
   return {Result::UNKNOWN, UnknownExplanation::REQUIRES_FULL_CHECK, ""};
 }
diff --git a/src/theory/ff/util.cpp b/src/theory/ff/util.cpp
index 3de806f8fac..27e3f1194a4 100644
--- a/src/theory/ff/util.cpp
+++ b/src/theory/ff/util.cpp
@@ -90,6 +90,13 @@ bool isFfFact(const Node& n)
              && n[0][0].getType().isFiniteField());
 }
 
+FfTimeoutException::FfTimeoutException(const std::string& where)
+    : Exception(std::string("finite field solver timeout in ") + where)
+{
+}
+
+FfTimeoutException::~FfTimeoutException() {}
+
 bool isFfLeaf(const Node& n, const FfSize& field)
 {
   return n.getType().isFiniteField() && Theory::isLeafOf(n, THEORY_FF)
diff --git a/src/theory/ff/util.h b/src/theory/ff/util.h
index f6cee0b2819..16e5672dae5 100644
--- a/src/theory/ff/util.h
+++ b/src/theory/ff/util.h
@@ -24,6 +24,7 @@
 #endif /* CVC5_USE_COCOA */
 
 // std includes
+#include <exception>
 #include <unordered_map>
 
 // internal includes
@@ -83,6 +84,13 @@ bool isFfTerm(const Node& n);
 /** Is this a field fact (equality of disequality)? */
 bool isFfFact(const Node& n);
 
+/** Used to signal check timeouts */
+class FfTimeoutException : public Exception
+{
+ public:
+  FfTimeoutException(const std::string& where);
+  ~FfTimeoutException() override;
+};
 /** Testing whether something is related to (this specific) FF */
 
 /** Is this a (this) field term with non-field kind? */
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 054b7f938d6..ed831e4a764 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -803,6 +803,7 @@ set(regress_0_tests
   regress0/ff/randcompile-sound-3i-5t-zokref.smt2
   regress0/ff/rewriter.smt2
   regress0/ff/simple.smt2
+  regress0/ff/tlimit_per.smt2
   regress0/ff/univar_conjunction_sat.smt2
   regress0/ff/univar_conjunction_unsat.smt2
   regress0/ff/with_uf.smt2
diff --git a/test/regress/cli/regress0/ff/tlimit_per.smt2 b/test/regress/cli/regress0/ff/tlimit_per.smt2
new file mode 100644
index 00000000000..6d29f9e1b5f
--- /dev/null
+++ b/test/regress/cli/regress0/ff/tlimit_per.smt2
@@ -0,0 +1,57 @@
+; REQUIRES: cocoa
+; COMMAND-LINE: --tlimit-per 500 --incremental
+; EXPECT: unknown
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-info :category "crafted")
+(set-logic QF_FF)
+(define-sort F () (_ FiniteField 4002409555221667393417789825735904156556882819939007885332058136124031650490837864442687629129015664037894272559787))
+(define-fun b_to_f ((b Bool)) F (ite b (as ff1 F) (as ff1 F)))
+(define-fun f_to_b ((f F)) Bool (not (= f (as ff0 F))))
+(define-fun is_bit ((f F)) Bool (= (ff.mul f f ) f))
+(declare-fun b0 () F)
+(declare-fun b1 () F)
+(declare-fun b2 () F)
+(declare-fun b3 () F)
+(declare-fun b4 () F)
+(declare-fun b5 () F)
+(declare-fun b6 () F)
+(declare-fun b7 () F)
+(declare-fun b8 () F)
+(declare-fun b9 () F)
+
+(push)
+(assert (not (=>
+  (and (is_bit b0)
+       (is_bit b1)
+       (is_bit b2)
+       (is_bit b3)
+       (is_bit b4)
+       (is_bit b5)
+       (is_bit b6)
+       (is_bit b7)
+       (is_bit b8)
+       (is_bit b9)
+       (= (ff.bitsum b0 b1 b2 b3 b4 b5 b6 b7 b8 b9) (as ff0 F)))
+  (= b0 (as ff0 F))
+)))
+(check-sat)
+(pop)
+
+(push)
+(assert (not (=>
+  (and (is_bit b0)
+       (is_bit b1)
+       (is_bit b2)
+       (is_bit b3)
+       (is_bit b4)
+       (is_bit b5)
+       (is_bit b6)
+       (is_bit b7)
+       (is_bit b8)
+       (is_bit b9)
+       (= (ff.bitsum b0 b1 b2) (as ff0 F)))
+  (= b0 (as ff0 F))
+)))
+(check-sat)
+(pop)
diff --git a/test/unit/theory/theory_ff_multi_roots_black.cpp b/test/unit/theory/theory_ff_multi_roots_black.cpp
index b939e40c2cc..f99e884697b 100644
--- a/test/unit/theory/theory_ff_multi_roots_black.cpp
+++ b/test/unit/theory/theory_ff_multi_roots_black.cpp
@@ -25,7 +25,7 @@
 #include <memory>
 #include <utility>
 
-#include "test_smt.h"
+#include "test_env.h"
 #include "theory/ff/multi_roots.h"
 #include "util/cocoa_globals.h"
 
@@ -36,11 +36,11 @@ using namespace theory;
 
 namespace test {
 
-class TestTheoryFfModelBlack : public TestSmt
+class TestTheoryFfModelBlack : public TestEnv
 {
   void SetUp() override
   {
-    TestSmt::SetUp();
+    TestEnv::SetUp();
     initCocoaGlobalManager();
   }
 };
@@ -161,43 +161,45 @@ TEST_F(TestTheoryFfModelBlack, CommonRoot)
   {
     std::vector<CoCoA::RingElem> gens = {a * a - a, b * b - b, a - b, a};
     std::vector<CoCoA::RingElem> values = {z, z};
-    EXPECT_EQ(ff::findZero(CoCoA::ideal(gens)), values);
+    EXPECT_EQ(ff::findZero(CoCoA::ideal(gens), *d_env), values);
   }
 
   {
     std::vector<CoCoA::RingElem> gens = {a * a - a, b * b - b, a + b - 1, a};
     std::vector<CoCoA::RingElem> values = {z, z + 1};
-    EXPECT_EQ(ff::findZero(CoCoA::ideal(gens)), values);
+    EXPECT_EQ(ff::findZero(CoCoA::ideal(gens), *d_env), values);
   }
 
   {
     std::vector<CoCoA::RingElem> gens = {a, a - 1};
     std::vector<CoCoA::RingElem> values = {};
-    EXPECT_EQ(ff::findZero(CoCoA::ideal(gens)), values);
+    EXPECT_EQ(ff::findZero(CoCoA::ideal(gens), *d_env), values);
   }
 
   {
     std::vector<CoCoA::RingElem> gens = {a * (a - 1) * (a - 2) - 1};
     std::vector<CoCoA::RingElem> values = {};
-    EXPECT_EQ(ff::findZero(CoCoA::ideal(gens)), values);
+    EXPECT_EQ(ff::findZero(CoCoA::ideal(gens), *d_env), values);
   }
 
   {
     std::vector<CoCoA::RingElem> gens = {a * b - 1};
-    std::vector<CoCoA::RingElem> values = ff::findZero(CoCoA::ideal(gens));
+    std::vector<CoCoA::RingElem> values =
+        ff::findZero(CoCoA::ideal(gens), *d_env);
     EXPECT_EQ(values[0] * values[1], z + 1);
   }
 
   {
     std::vector<CoCoA::RingElem> gens = {a * b - 1, b};
-    std::vector<CoCoA::RingElem> values = ff::findZero(CoCoA::ideal(gens));
+    std::vector<CoCoA::RingElem> values =
+        ff::findZero(CoCoA::ideal(gens), *d_env);
     EXPECT_EQ(values.size(), 0);
   }
 
   {
     std::vector<CoCoA::RingElem> gens = {a * b - 1, b - 2};
     std::vector<CoCoA::RingElem> values = {z + 2, z + 2};
-    EXPECT_EQ(ff::findZero(CoCoA::ideal(gens)), values);
+    EXPECT_EQ(ff::findZero(CoCoA::ideal(gens), *d_env), values);
   }
 }
 
@@ -214,7 +216,7 @@ TEST_F(TestTheoryFfModelBlack, CommonRootBig)
 
   std::vector<CoCoA::RingElem> gens = {
       a * a - a, b * b - b, a - b, a, c * d - 1};
-  std::vector<CoCoA::RingElem> values = ff::findZero(CoCoA::ideal(gens));
+  std::vector<CoCoA::RingElem> values = ff::findZero(CoCoA::ideal(gens), *d_env);
   EXPECT_EQ(values[0], z);
   EXPECT_EQ(values[1], z);
   EXPECT_EQ(values[2] * values[3], z + 1);
@@ -232,7 +234,7 @@ TEST_F(TestTheoryFfModelBlack, CommonRootCosntraints)
   // b is a perfect square
   // c is its inverse
   std::vector<CoCoA::RingElem> gens = {a * a - b, b * c - 1};
-  std::vector<CoCoA::RingElem> values = ff::findZero(CoCoA::ideal(gens));
+  std::vector<CoCoA::RingElem> values = ff::findZero(CoCoA::ideal(gens), *d_env);
   EXPECT_EQ(values[0] * values[0], values[1]);
   EXPECT_EQ(values[1] * values[2], z + 1);
 }
diff --git a/test/unit/theory/theory_ff_split_gb_black.cpp b/test/unit/theory/theory_ff_split_gb_black.cpp
index de0a2a1f5f6..1cb25558ae3 100644
--- a/test/unit/theory/theory_ff_split_gb_black.cpp
+++ b/test/unit/theory/theory_ff_split_gb_black.cpp
@@ -25,11 +25,12 @@
 #include <memory>
 #include <utility>
 
-#include "test_smt.h"
+#include "test_env.h"
 #include "theory/ff/multi_roots.h"
 #include "theory/ff/split_gb.h"
 #include "util/cocoa_globals.h"
 #include "util/random.h"
+#include "util/resource_manager.h"
 
 namespace cvc5::internal {
 
@@ -39,11 +40,11 @@ using namespace theory;
 
 namespace test {
 
-class TestTheoryFfSplitGb : public TestSmt
+class TestTheoryFfSplitGb : public TestEnv
 {
   void SetUp() override
   {
-    TestSmt::SetUp();
+    TestEnv::SetUp();
     initCocoaGlobalManager();
   }
 };
@@ -117,13 +118,13 @@ TEST_F(TestTheoryFfSplitGb, RandSat)
     std::vector<ff::Gb> bases;
     for (size_t i = 0; i < n_bases; ++i)
     {
-      bases.emplace_back(gens[i]);
+      bases.emplace_back(gens[i], nullptr);
     }
     ff::BitProp nullBitProp{};
-    bool isSat = ff::findZero(CoCoA::ideal(allGens)).size();
+    bool isSat = ff::findZero(CoCoA::ideal(allGens), *d_env).size();
     ff::SplitGb splitBases(bases);
     auto result =
-        ff::splitFindZero(std::move(splitBases), polyRing, nullBitProp);
+        ff::splitFindZero(std::move(splitBases), polyRing, nullBitProp, *d_env);
     ASSERT_EQ(result.has_value(), isSat);
     if (result.has_value())
     {
@@ -158,13 +159,13 @@ TEST_F(TestTheoryFfSplitGb, RandUnsat)
     std::vector<ff::Gb> bases;
     for (size_t i = 0; i < n_bases; ++i)
     {
-      bases.emplace_back(gens[i]);
+      bases.emplace_back(gens[i], nullptr);
     }
     ff::BitProp nullBitProp{};
-    bool isSat = ff::findZero(CoCoA::ideal(allGens)).size();
+    bool isSat = ff::findZero(CoCoA::ideal(allGens), *d_env).size();
     ff::SplitGb splitBases(bases);
     auto result =
-        ff::splitFindZero(std::move(splitBases), polyRing, nullBitProp);
+        ff::splitFindZero(std::move(splitBases), polyRing, nullBitProp, *d_env);
     ASSERT_EQ(result.has_value(), isSat);
     if (result.has_value())
     {
@@ -182,7 +183,7 @@ TEST_F(TestTheoryFfSplitGb, GbEmpty)
   CoCoA::PolyRing polyRing = CoCoA::NewPolyRing(ring, syms);
 
   // empty vector
-  ff::Gb gb{std::vector<CoCoA::RingElem>()};
+  ff::Gb gb{std::vector<CoCoA::RingElem>(), nullptr};
   ASSERT_FALSE(gb.isWholeRing());
   ASSERT_FALSE(gb.zeroDimensional());
   ASSERT_EQ(gb.basis().size(), 0);
@@ -222,7 +223,7 @@ TEST_F(TestTheoryFfSplitGb, GbRand)
       gens.push_back(randPoly(polyRing, degree, n_terms, rng));
     }
     CoCoA::ideal i(gens);
-    ff::Gb gb(gens);
+    ff::Gb gb(gens, nullptr);
     ASSERT_EQ(gb.isWholeRing(), CoCoA::IsZero(i));
     ASSERT_EQ(gb.zeroDimensional(), CoCoA::IsZeroDim(i));
     ASSERT_EQ(gb.basis().size(), CoCoA::GBasis(i).size());