diff --git a/DEVELOPING.md b/DEVELOPING.md
index 6ed05fa..cc2c221 100644
--- a/DEVELOPING.md
+++ b/DEVELOPING.md
@@ -73,6 +73,12 @@
     source ~/.bashrc
     ```
 
+1. (Optional) Set path to custom files (see `SMTD_CUSTOM.md` for more information)
+    ```bash
+    echo 'export SMTD_CUSTOM_PATH=<PATH_TO_SMTD_CUSTOM>' >> ~/.bashrc
+    source ~/.bashrc
+    ```
+
 1. Run build script
 
     Begin in project root:
@@ -162,6 +168,12 @@
     source ~/.bashrc
     ```
 
+1. (Optional) Set path to custom files (see `SMTD_CUSTOM.md` for more information)
+    ```bash
+    echo 'export SMTD_CUSTOM_PATH=<PATH_TO_SMTD_CUSTOM>' >> ~/.bashrc
+    source ~/.bashrc
+    ```
+
 1. Run build script
     Begin in project root:
     ```bash
@@ -179,10 +191,10 @@
     pip install hatch
     ```
 
-1. Update `.zshrc` (or `.bashrc`)
+1. Update `.bashrc` (or `.zshrc`)
 
     ```bash
-    echo 'export PATH="/opt/homebrew/opt/bison/bin:$PATH"' >> ~/.zshrc
+    echo 'export PATH="/opt/homebrew/opt/bison/bin:$PATH"' >> ~/.bashrc
     ```
 
 3. Use ***Python 3.11*** -- here's one way (other versions of Python may not work)
@@ -238,6 +250,12 @@
     source ~/.bashrc
     ```
   
+1. (Optional) Set path to custom files (see `SMTD_CUSTOM.md` for more information)
+    ```bash
+    echo 'export SMTD_CUSTOM_PATH=<PATH_TO_SMTD_CUSTOM>' >> ~/.bashrc
+    source ~/.bashrc
+    ```
+
 1. Run the build script
 
     Begin in project root:
diff --git a/SMTD_CUSTOM.md b/SMTD_CUSTOM.md
new file mode 100644
index 0000000..d6858ff
--- /dev/null
+++ b/SMTD_CUSTOM.md
@@ -0,0 +1,41 @@
+This file describes how to implement features that are factored out of the main SMT-D repo. 
+
+#### Prerequistes 
+* Everything from `DEVELOPING.md` 
+* Set `$SMTD_CUSTOM_PATH` to the absolute path to the folder hosting the custom features, called `smtd_custom`. For example, `/home/<username>/smtd_custom`
+#### Custom worker heuristics
+* In the `smtd_custom/custom_worker_heuristics` folder, implement `CustomHeuristics.cpp` and `CustomHeuristics.h`, 
+  which implement the `UserHeuristics.h` interface 
+* Pass argument `--custom_worker` when running `./run_build.sh` (building SMT-D)
+#### Custom proto fields
+* In the `smtd_custom/custom_proto` folder, implement `custom_proto.proto`. A minimal example of `custom_proto.proto` 
+  is as follows (you must use the `SmtD` package and use, at least, the `SmtDWrapperCustomOptions` struct): 
+    ```
+    syntax = "proto3";
+    package SmtD;
+
+    message SmtDWrapperCustomOptions {
+        uint32 custom = 1;
+    }
+    ```
+* Pass argument `--custom_proto` when running `./run_build.sh` (building SMT-D)
+#### Custom stats reporting
+* In the `smtd_custom/custom_stats` folder, implement `custom_stats_handler.py`, which implements the 
+  interface defined in `UserStatsHandler.py` in SMT-D
+* Pass argument `--user_stats` when running SMT-D (e.g., `./smtd -f <file> --user_stats`)
+* Also pass argument `--broker user` when calling SMT-D. (In the future, the user broker will 
+  become the only broker, and all the clause sharing heuristics will be modularly defined, 
+  rather than having a separate parse broker, rate broker, and so on. When this time comes, 
+  it will be possible to, for example, mix the parse time heuristic with user stats handling. 
+  But for now, it is unsupported.)
+#### Custom control loops (clause sharing heuristics)
+* In the `smtd_custom/custom_control_loops` folder, implement `custom_control_loop.py`, which implements 
+  the interface defined in `UserControlLoop.py`
+* Pass argument `--user_control_loop` when running SMT-D
+* Also pass argument `--broker user` when calling SMT-D
+#### Miscellaneous
+* In the build script, when `--custom_worker` or `--custom_proto` is not passed, 
+  a default, dummy value for `custom_proto.proto` and `CustomHeuristics.cpp/h` is 
+  generated by the build script (`./run_build.sh`). Hence, if you ever update the interface for 
+  custom workers or proto files, you will also need to update the build script accordingly. 
+  There is probably a better way of doing this.
diff --git a/run_build.sh b/run_build.sh
index 5013199..c4b1a3b 100755
--- a/run_build.sh
+++ b/run_build.sh
@@ -1,11 +1,15 @@
 #!/usr/bin/env bash
 # Args
-#   --only_broker -> only run broker portions of build script
-#   --only_worker -> only run worker portions of build script
-#   --debug       -> build worker executable in debug mode
+#   --only_broker  -> only run broker portions of build script
+#   --only_worker  -> only run worker portions of build script
+#   --debug        -> build worker executable in debug mode
+#   --custom_proto -> include user-defined .proto file from ${SMTD_CUSTOM_PATH}/custom_proto/custom_proto.proto
+#   --custom_worker -> include user-defined .cpp/.h files from ${SMTD_CUSTOM_PATH}/custom_worker_heuristics/CustomHeuristics.cpp/.h
 #   You can use any combination of the above args, but combining --only_broker with --only_worker
 #   will perform no action.
 
+# TODO: Allow passing filename of custom proto and custom worker files
+
 cd "$(dirname "$0")" || exit 1
 
 if [ -z "${SMTD_CVC5_REPO_PATH}" ]; then
@@ -24,6 +28,49 @@ if ! [[ " $@ " == *" --only_worker "* ]]; then
   find ./src/smtd/proto -maxdepth 1 -type f \( -name "*.py" -o -name "*.pyi" \) -exec rm -f {} +
   touch ./src/smtd/proto/__init__.py
 
+  # Copy custom proto file to proto directory
+  if [[ " $@ " == *" --custom_proto "* ]]; then
+    if [ -z "${SMTD_CUSTOM_PATH}" ]; then
+      echo "Error: SMTD_CUSTOM_PATH is not set. See DEVELOPING.md"  >&2
+      exit 1
+    fi
+
+    cp ${SMTD_CUSTOM_PATH}/custom_proto/custom_proto.proto ./src/smtd/proto/custom_proto.proto
+  else 
+    echo "syntax = \"proto3\";
+          package SmtD;
+
+          message SmtDWrapperCustomOptions {
+            uint32 custom = 1;
+          }" > ./src/smtd/proto/custom_proto.proto
+  fi
+
+  # Copy custom worker heuristics file to worker science directory
+  if [[ " $@ " == *" --custom_worker "* ]]; then
+    if [ -z "${SMTD_CUSTOM_PATH}" ]; then
+      echo "Error: SMTD_CUSTOM_PATH is not set. See DEVELOPING.md"  >&2
+      exit 1
+    fi
+
+    cp ${SMTD_CUSTOM_PATH}/custom_worker_heuristics/CustomHeuristics.cpp ./src/smtd/workers/src/science/CustomHeuristics.cpp
+    cp ${SMTD_CUSTOM_PATH}/custom_worker_heuristics/CustomHeuristics.h ./src/smtd/workers/src/science/CustomHeuristics.h
+  else 
+    echo "#include <iostream>
+          #include \"CustomHeuristics.h\"
+
+          void CustomHeuristics::dummy(SmtD::SmtDStatus &d_stats, std::optional<std::reference_wrapper<const cvc5::Term>> lemma, SemiStructuredContext &ssctx, SmtDWorkerInterface &d_interface) {
+              return;
+          }" > ./src/smtd/workers/src/science/CustomHeuristics.cpp
+    echo "#ifndef CVC5__CUSTOM_HEURISTICS_H
+          #define CVC5__CUSTOM_HEURISTICS_H
+          #include \"UserHeuristics.h\"
+          class CustomHeuristics : public UserHeuristics {
+          public:
+              void dummy(SmtD::SmtDStatus &d_stats, std::optional<std::reference_wrapper<const cvc5::Term>> lemma, SemiStructuredContext &ssctx, SmtDWorkerInterface &d_interface) override;
+              };
+          #endif " > ./src/smtd/workers/src/science/CustomHeuristics.h
+  fi
+
   # Ideally: Put all generated stuff in a top-level build folder
   hatch run python3.11 -m grpc_tools.protoc \
     --python_out=./src \
diff --git a/src/smtd/broker/main.py b/src/smtd/broker/main.py
index 0fdbfb5..97e3dc7 100644
--- a/src/smtd/broker/main.py
+++ b/src/smtd/broker/main.py
@@ -19,6 +19,7 @@
 from smtd.broker.science.brokers.parse_time_broker import parse_time_broker
 from smtd.broker.science.brokers.rate_broker import rate_broker
 from smtd.broker.science.brokers.size_broker import size_broker
+from smtd.broker.science.brokers.user_broker import user_broker
 from smtd.broker.science.ClusterMap import ClusterMap
 from smtd.broker.science.statistics.formatting_helpers import (
     parse_key_value_pairs,
@@ -54,8 +55,9 @@ async def async_entry():
     else:
         cluster_config = {"partitioners": []}
 
+    optional_env_vars = ["SMTD_CUSTOM_PATH"]
     for var, val in config.items():
-        if val is None:
+        if val is None and not var in optional_env_vars:
             # TODO: Update when creating first release -- non-developer users should not be directed to DEVELOPING.md
             logging.error(f"Environment variable {var} is not set. See DEVELOPING.md")
             raise FileNotFoundError
@@ -95,6 +97,7 @@ async def async_entry():
                 "size": size_broker,
                 "rate": rate_broker,
                 "parse": parse_time_broker,
+                "user": user_broker,
             }[args.broker]
             logging.warning(f"Using {broker_implementation}.")
             winner, result, winner_duration = await broker_implementation(
diff --git a/src/smtd/broker/parse_args.py b/src/smtd/broker/parse_args.py
index 7e4b03c..6f3b75c 100644
--- a/src/smtd/broker/parse_args.py
+++ b/src/smtd/broker/parse_args.py
@@ -30,6 +30,12 @@
 parser.add_argument(
     "--share_theory_lemma", action="store_true", help="Share theory lemmas (default: False)"
 )
+parser.add_argument(
+    "--user_stats", action="store_true", help="Use user-implemented statistics (default: False)"
+)
+parser.add_argument(
+    "--user_control_loop", action="store_true", help="Use user-implemented control loop (default: False)"
+)
 
 # old is now unsupported since it relies heavily on strings, and is not easily portable to atom caching
 # parser.add_argument('--broker', type=str, default='old', choices=['old', 'size', 'rate', 'weighted', 'parse'], help='Broker strategy to use.')
@@ -37,7 +43,7 @@
     "--broker",
     type=str,
     default="parse",
-    choices=["size", "rate", "weighted", "parse"],
+    choices=["size", "rate", "weighted", "parse", "user",],
     help="Broker strategy to use.",
 )
 parser.add_argument(
@@ -181,7 +187,7 @@
     "--scrambler_seed",
     type=int,
     default=100,
-    help="Seed for scrambler (default: 100; DO NOT USE 0!!)",
+    help="Seed for scrambler (default: 100; DO NOT USE 0!)",
 )
 parser.add_argument(
     "--scrambler_shuffle_decls",
diff --git a/src/smtd/broker/parse_config.py b/src/smtd/broker/parse_config.py
index 7a1c614..b70944a 100644
--- a/src/smtd/broker/parse_config.py
+++ b/src/smtd/broker/parse_config.py
@@ -1,6 +1,6 @@
 import os
 
-env_variables = ["SMTD_CVC5_REPO_PATH", "SMTD_SCRAMBLER_PATH"]
+env_variables = ["SMTD_CVC5_REPO_PATH", "SMTD_SCRAMBLER_PATH", "SMTD_CUSTOM_PATH"]
 
 # Config dictionary is for non-user-configurable relative paths within the project,
 # as well as for external dependencies fetched from environment variables.
@@ -14,4 +14,4 @@
 
 # TODO: move all build artifacts to to top-level 'build' directory
 config["WORKER_EXE_PATH"] = "src/smtd/workers/build-release/smtd-worker"
-config["PROTO_DIR_PATH"] = "src/smtd/proto/"
+config["PROTO_DIR_PATH"] = "src/smtd/proto/"
\ No newline at end of file
diff --git a/src/smtd/broker/science/SemiStructuredContext.py b/src/smtd/broker/science/SemiStructuredContext.py
index 478743c..199c5c4 100644
--- a/src/smtd/broker/science/SemiStructuredContext.py
+++ b/src/smtd/broker/science/SemiStructuredContext.py
@@ -9,10 +9,10 @@
 from smtd.broker.science.statistics.formatting_helpers import n5
 from smtd.broker.systems.servers.SmtDWorker import SmtDWorker
 from smtd.broker.systems.SmtDBrokerInterface import SmtDBrokerInterface
-from smtd.proto import semi_structured_api_pb2 as soapi
+from smtd.proto import semi_structured_api_pb2 as ssapi
 from smtd.proto import service_api_pb2 as pb
 
-UUID_t = soapi.SmtSemiStructuredDefinitionUUID
+UUID_t = ssapi.SmtSemiStructuredDefinitionUUID
 
 
 def _u2p(uuid):
@@ -50,7 +50,7 @@ def __init__(self):
     def synchronize_definition(
         self,
         sender: SmtDWorker,
-        d: soapi.SmtSemiStructuredDefinition,
+        d: ssapi.SmtSemiStructuredDefinition,
         interface: SmtDBrokerInterface,
     ):
         self.unmapping[_u2p(d.new_uuid)] = d.str
@@ -75,12 +75,12 @@ def synchronize_definition(
             self.unique_atom_stats[sender] += 1
             # for s in interface.workers: self.knows_about[s].add(_u2p(d.uuid))
 
-    def to_string(self, l: soapi.SmtSemiStructuredExpression) -> str:
+    def to_string(self, l: ssapi.SmtSemiStructuredExpression) -> str:
         if l.HasField("connective"):
             prefix = {
-                soapi.OR: "(or ",
-                soapi.AND: "(and ",
-                soapi.NOT: "(not ",
+                ssapi.OR: "(or ",
+                ssapi.AND: "(and ",
+                ssapi.NOT: "(not ",
             }[l.connective.kind]
             infix = " ".join(self.to_string(c) for c in l.connective.children)
             suffix = ")"
@@ -88,7 +88,7 @@ def to_string(self, l: soapi.SmtSemiStructuredExpression) -> str:
         else:
             return self.unmapping.get(pair := _u2p(l.uuid), f"<< unknown uuid {pair} >>")
 
-    # def remap(self, sender: SmtDWorker, l: soapi.SmtSemiStructuredExpression):
+    # def remap(self, sender: SmtDWorker, l: ssapi.SmtSemiStructuredExpression):
     #     # todo: we can sort the children and maybe do some deduplication here if we want.
     #     if l.HasField('uuid'):
     #         remapped_uuid = self.remapping.get(_u2p(l.uuid))
@@ -99,7 +99,7 @@ def to_string(self, l: soapi.SmtSemiStructuredExpression) -> str:
     #         for c in l.connective.children:
     #             self.remap(sender, c)
 
-    # def safe_to_send(self, l: soapi.SmtSemiStructuredExpression, to: SmtDWorker):
+    # def safe_to_send(self, l: ssapi.SmtSemiStructuredExpression, to: SmtDWorker):
     #     if l.HasField('uuid'):
     #         if _u2p(l.uuid) not in self.knows_about[to]:
     #             logging.error(f"Attempting to send lemma containing UUID {l.uuid} (which was remapped to {self.remapping.get(_u2p(l.uuid))}) to worker {to} which does not know about that UUID.")
diff --git a/src/smtd/broker/science/brokers/parse_time_broker.py b/src/smtd/broker/science/brokers/parse_time_broker.py
index 9f9489d..6f3102f 100644
--- a/src/smtd/broker/science/brokers/parse_time_broker.py
+++ b/src/smtd/broker/science/brokers/parse_time_broker.py
@@ -217,6 +217,7 @@ async def parse_time_broker(
                     interface.export_immediate(req, to_specific_workers={sender})
 
                 if message.HasField("define"):
+                    # print("PROCESSING DEFINE MESSAGE")
                     ssctx.synchronize_definition(sender, message.define, interface)
 
                 if message.HasField("lemma"):
@@ -226,7 +227,7 @@ async def parse_time_broker(
                     if message.lemma.metadata.length == 1:
                         if args.log_unit_clauses:
                             logging.info(
-                                f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.soapi)[:100]}`... was discovered by {sender}"
+                                f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.ssapi)[:100]}`... was discovered by {sender}"
                             )
                         stats.incr("unit_clauses", sender, +1)
 
@@ -238,7 +239,7 @@ async def parse_time_broker(
                     ), "weighted broker does not support partitioning yet."
 
                     fwd = pb.ToSmtDMessage()
-                    fwd.lemma.expr.soapi.CopyFrom(message.lemma.expr.soapi)
+                    fwd.lemma.expr.ssapi.CopyFrom(message.lemma.expr.ssapi)
                     for receiver in interface.workers - {sender}:
                         current_adaptive_share_length = share_length_controllers[receiver].output
                         if message.lemma.metadata.length <= current_adaptive_share_length:
diff --git a/src/smtd/broker/science/brokers/rate_broker.py b/src/smtd/broker/science/brokers/rate_broker.py
index 8d0ad6d..f5d9f27 100644
--- a/src/smtd/broker/science/brokers/rate_broker.py
+++ b/src/smtd/broker/science/brokers/rate_broker.py
@@ -169,7 +169,7 @@ async def rate_broker(
                     )  # we don't support more than 1 formula currently
                     if args.log_unit_clauses:
                         logging.info(
-                            f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.soapi)[:100]}`... was discovered by {sender}"
+                            f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.ssapi)[:100]}`... was discovered by {sender}"
                         )
                     if message.lemma.metadata.length == 1:
                         stats.incr("unit_clauses", sender, +1)
diff --git a/src/smtd/broker/science/brokers/size_broker.py b/src/smtd/broker/science/brokers/size_broker.py
index 3e65bd1..d53f736 100644
--- a/src/smtd/broker/science/brokers/size_broker.py
+++ b/src/smtd/broker/science/brokers/size_broker.py
@@ -26,7 +26,7 @@
 from smtd.broker.science.statistics.SimpleStatsHandler import SimpleStatsHandler
 from smtd.broker.systems.servers.LocalSmtDWorker import LocalSmtDWorker
 from smtd.broker.systems.SmtDBrokerInterface import SmtDBrokerInterface
-from smtd.proto import semi_structured_api_pb2 as soapi
+from smtd.proto import semi_structured_api_pb2 as ssapi
 from smtd.proto import service_api_pb2 as pb
 
 
@@ -136,7 +136,7 @@ async def size_broker(
                     )  # we don't support more than 1 formula currently
                     if args.log_unit_clauses:
                         logging.info(
-                            f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.soapi)[:100]}`... was discovered by {sender}"
+                            f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.ssapi)[:100]}`... was discovered by {sender}"
                         )
                     if message.lemma.metadata.length == 1:
                         stats.incr("unit_clauses", sender, +1)
@@ -151,7 +151,7 @@ async def size_broker(
                     assert message.lemma.metadata.length <= args.max_share_length
 
                     sent_msg = pb.ToSmtDMessage()
-                    sent_msg.lemma.expr.soapi.CopyFrom(message.lemma.expr.soapi)
+                    sent_msg.lemma.expr.ssapi.CopyFrom(message.lemma.expr.ssapi)
                     interface.export_immediate(
                         sent_msg, to_specific_workers=interface.workers - {sender}
                     )
diff --git a/src/smtd/broker/science/brokers/user_broker.py b/src/smtd/broker/science/brokers/user_broker.py
new file mode 100644
index 0000000..68ad4cd
--- /dev/null
+++ b/src/smtd/broker/science/brokers/user_broker.py
@@ -0,0 +1,358 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+import asyncio
+import logging
+import time
+import sys
+from argparse import Namespace
+from typing import Dict, FrozenSet, Iterable, List, Optional, Set, Tuple
+from parse_config import config
+from pathlib import Path
+
+import numpy as np
+import tabulate
+import os
+
+from smtd.broker.science.brokers.broker_utils import (
+    handle_heartbeat_telemetry,
+    judge_potential_winner,
+    run_scrambler,
+    smtfile_get_logic,
+    write_cluster_result,
+)
+from smtd.broker.science.ClusterMap import ClusterMap
+
+from smtd.broker.science.cvc5_options import (
+    get_cvc5_options_fmcad24,
+    get_logic_options,
+    options_to_flags,
+    parse_options,
+)
+from smtd.broker.science.SemiStructuredContext import SemiStructuredContext
+from smtd.broker.science.statistics import AbstractStatsHandler
+from smtd.broker.science.statistics.AsciiTableStatsHandler import AsciiTableStatsHandler
+from smtd.broker.science.statistics.formatting_helpers import n5, p2, result_short_str
+from smtd.broker.science.statistics.SetupTeardownTimer import SetupTeardownTimer
+from smtd.broker.science.statistics.SimpleStatsHandler import SimpleStatsHandler
+from smtd.broker.science.control_loops.UserControlLoop import UserControlLoop
+from smtd.broker.systems.servers.LocalSmtDWorker import LocalSmtDWorker
+from smtd.broker.systems.SmtDBrokerInterface import SmtDBrokerInterface
+from smtd.proto import service_api_pb2 as pb
+
+async def user_broker(
+    req: pb.SmtDSolveRequest,
+    interface: SmtDBrokerInterface,
+    args: Namespace,
+    cm: ClusterMap,
+    config: Dict[str, str],
+):
+    # NOTE: In theory, these imports will work because the user has specified they want to use the 
+    #       user broker. But we probably want to fail gracefully if these imports don't work
+    #       (in the case where the user passes --broker user but does not have definitions for 
+    #       CustomControlLoop or CustomStatsHandler)
+    if config["SMTD_CUSTOM_PATH"]:
+        custom_path = Path(config["SMTD_CUSTOM_PATH"]+"/..").resolve()
+        sys.path.append(str(custom_path))
+
+        # NOTE: Default behavior of this broker is the same as the size broker until CustomControlLoop is updated
+        from smtd_custom.custom_control_loops.custom_control_loop import CustomControlLoop
+        from smtd_custom.custom_stats.custom_stats_handler import CustomStatsHandler
+    # User stats and user broker both require an $SMTD_CUSTOM_PATH
+    elif args.user_stats or args.user_control_loop:
+        logging.error("User broker requires $SMTD_CUSTOM_PATH to be set if using --user_stats or --user_control_loop. See DEVELOPING.MD")
+        raise FileNotFoundError
+
+    start_time = 0
+    ssctx = SemiStructuredContext()
+
+    winner = None
+    winner_duration = -1.0
+
+    # todo: 'smt_filenames' should come from 'run_scrambler'
+    #       Scrambler temporarily removed while we propose a PR for the public version 
+    #       This will break if formula isn't given as a filepath
+    #       Next three lines should be deleted
+    fmt = req.formula.expr.WhichOneof("format")
+    assert fmt in {"filepath"}, f"Unsupported formula format '{fmt}'."
+    smt_filenames = [req.formula.expr.filepath] * len(interface.workers)
+    #smt_filenames = run_scrambler(interface, req, args, config)
+
+    
+    strategies, _, _ = get_logic_options(args, smtfile_get_logic(smt_filenames[0]))
+    if args.user_stats:
+        stats = CustomStatsHandler(interface, cm, len(strategies))
+    else:
+        stats = AsciiTableStatsHandler(interface, cm, len(strategies))
+
+    if args.user_control_loop:
+        share_length_controllers = {
+            receiver: CustomControlLoop(
+                gain_kP=0.02 * 16 / len(interface.workers),
+                target=args.target_parse_time,
+                initial_output=args.max_share_length,
+                min_output=2,
+                max_output=args.max_share_length,
+                stats=stats
+            )
+            for receiver in interface.workers
+        }
+    else: 
+        share_length_controllers = {
+            receiver: UserControlLoop(
+                gain_kP=0.02 * 16 / len(interface.workers),
+                target=args.target_parse_time,
+                initial_output=args.max_share_length,
+                min_output=2,
+                max_output=args.max_share_length
+            )
+            for receiver in interface.workers
+        }
+
+    assert not args.throughput_test, "user broker does not support throughput tests."
+    assert not cm.pleader_to_partition, "user broker does not support partitioning yet."
+    assert not cm.pworker_to_partition, "user broker does not support partitioning yet."
+    assert not cm.noisy_workers, "user broker does not support noisy workers."
+
+    assert len(interface.workers) > 1, f"user broker does not work with single workers."
+
+    try:
+        # step 0: respect the user's desired timeout
+        # (will throw exception after timeout_secs, hence try-finally.)
+        async with asyncio.timeout(req.timeout_secs):
+
+            # step 1: tell everyone what they're going to run
+            # maybe do partitioning or something else fancy later
+            for idx, s in enumerate(sorted(interface.workers, key=lambda worker: worker.port)):
+                targeted_req: pb.ToSmtDMessage = pb.ToSmtDMessage()
+                targeted_req.request.CopyFrom(req)
+
+                smt_logic = smtfile_get_logic(smt_filenames[idx])
+                logging.info(f"SMT logic from query: {smt_logic}")
+
+                targeted_req.request.formula.expr.filepath = smt_filenames[idx]
+
+                options = get_cvc5_options_fmcad24(idx, smt_logic, args, False)
+                options = parse_options(options)
+
+                logging.info(f"RUN-COMMAND: {options_to_flags(options)}")
+                targeted_req.request.options.CopyFrom(options)
+
+                interface.export_immediate(targeted_req, to_specific_workers={s})
+                
+                logging.warning(f"Sent formula with seed {idx} to worker {s}.")
+
+            await interface.relinquish_execution()  # actually send the messages
+            start_time = time.time()
+            last_print_time = time.time()
+
+            SetupTeardownTimer.begin(SetupTeardownTimer.Phases.RUN_SOLVE)
+            while True:
+                await interface.relinquish_execution()
+
+                if time.time() - last_print_time > 2:
+                    last_print_time = time.time()
+                    stats.handle_user_stats({"share_length_controllers": share_length_controllers})
+                    stats.print()
+                    ssctx.print_stats(stats)
+
+                    logging.info(
+                        "Broker Real-Time Sharing Control Loops:\n"
+                        + tabulate.tabulate(
+                            tabular_data=[
+                                ["", "Avg."] + [f"#{i}" for i, _ in stats.workers],
+                                [
+                                    "instantaneous import time:",
+                                    p2(
+                                        sum(
+                                            share_length_controllers[s].lpf.value
+                                            for _, s in stats.workers
+                                        )
+                                        / len(stats.workers),
+                                        100,
+                                    ),
+                                ]
+                                + [
+                                    p2(share_length_controllers[s].lpf.value, 100)
+                                    for _, s in stats.workers
+                                ],
+                                [
+                                    "adaptive size limit:",
+                                    n5(
+                                        sum(
+                                            share_length_controllers[s].output
+                                            for _, s in stats.workers
+                                        )
+                                        / len(stats.workers)
+                                    ),
+                                ]
+                                + [
+                                    n5(share_length_controllers[s].output) for _, s in stats.workers
+                                ],
+                            ],
+                            headers="firstrow",
+                            disable_numparse=True,
+                            colalign=["right", "left"],
+                        )
+                    )
+
+                    if interface.pending_imports() > 10e3 * 16 / len(interface.workers):
+                        logging.warning(
+                            f"Broker is falling behind! Temporarily limiting max share length to 2."
+                        )
+                        for c in share_length_controllers.values():
+                            c.max_output = 2
+                        req = pb.ToSmtDMessage()
+                        req.adapt.share_length = 2
+                        interface.export_immediate(req, to_specific_workers=interface.workers)
+                    else:
+                        for c in share_length_controllers.values():
+                            c.max_output = args.max_share_length
+
+                    workers_crashed = (
+                        s.proc.poll() is not None
+                        for s in interface.workers
+                        if isinstance(s, LocalSmtDWorker)
+                    )
+                    if args.exit_on_worker_crash == "all" and all(workers_crashed):
+                        logging.error(f"All workers crashed. Exiting.")
+                        break
+                    elif args.exit_on_worker_crash == "any" and any(workers_crashed):
+                        logging.error(f"Some worker(s) crashed. Exiting.")
+                        break
+
+                sender_message = interface.import_immediate()
+                if sender_message is None:
+                    await interface.relinquish_execution()
+                    continue
+
+                sender, message = sender_message
+
+                assert (
+                    message.HasField("heartbeat")
+                    or message.HasField("define")
+                    or message.HasField("lemma")
+                    or message.HasField("result")
+                )
+
+                if message.HasField("heartbeat"):
+                    handle_heartbeat_telemetry(sender, message.heartbeat, cm, stats)
+                    share_length_controllers[sender].update_control_loop(
+                        {
+                            "total_cpu_time": message.heartbeat.still_running.total_plugin_import_time_ms,
+                            "total_elapsed_time": message.heartbeat.still_running.elapsed_wall_clock_time_ms,
+                        }
+                        # subtracting parse time because this can be very significant (20% cpu time) on the largest problems.
+                        # the idea is that with atom caching, the parse time will ultimately go back down
+                        # but we still want the worker to participate in the meantime.
+                        # this has been show to be faster on the largest (mostly SAT QF_LRA) problems
+                        # UPDATE: while it's good for an edge-case of QF_LRA problems, it's terrible for ALL string problems.
+                        # strings generate massive new atoms constantly, hammering the parser throughout the entire solve.
+                        # total_subtract_times=message.heartbeat.still_running.import_parse_time_ms
+                    )
+                    if args.user_control_loop:
+                        max_share_length = max(
+                            share_length_controllers[receiver].get_output({"sender": sender, "receiver": receiver})
+                            for receiver in interface.workers
+                            if sender != receiver
+                        )
+                    else:
+                        max_share_length = max(
+                            share_length_controllers[receiver].output
+                            for receiver in interface.workers
+                            if sender != receiver
+                        )
+                    req = pb.ToSmtDMessage()
+                    req.adapt.share_length = int(max_share_length + 2)  # a little buffer
+                    interface.export_immediate(req, to_specific_workers={sender})
+
+                if message.HasField("define"):
+                    # print("PROCESSING DEFINE MESSAGE")
+                    ssctx.synchronize_definition(sender, message.define, interface)
+
+                if message.HasField("lemma"):
+                    assert (
+                        message.lemma.formula_id == 0
+                    )  # we don't support more than 1 formula currently
+                    if message.lemma.metadata.length == 1:
+                        if args.log_unit_clauses:
+                            logging.info(
+                                f"Unit lemma/clause `{ssctx.to_string(message.lemma.expr.ssapi)[:100]}`... was discovered by {sender}"
+                            )
+                        stats.incr("unit_clauses", sender, +1)
+
+                    assert (
+                        not message.lemma.metadata.is_partitioning_assumption
+                    ), "weighted broker does not support partitioning yet."
+                    assert (
+                        not message.lemma.metadata.predicated_by
+                    ), "weighted broker does not support partitioning yet."
+
+                    fwd = pb.ToSmtDMessage()
+                    fwd.lemma.expr.ssapi.CopyFrom(message.lemma.expr.ssapi)
+                    for receiver in interface.workers - {sender}:
+                        if args.user_control_loop:
+                            current_adaptive_share_length = share_length_controllers[receiver].get_output({"sender": sender, "receiver": receiver})
+                        else:
+                            current_adaptive_share_length = share_length_controllers[receiver].output
+                        if message.lemma.metadata.length <= current_adaptive_share_length:
+                            interface.export_immediate(fwd, to_specific_workers={receiver})
+
+                if message.HasField("result"):
+                    assert message.result.HasField("ok") or message.result.HasField("err")
+                    cm.worker_to_result[sender] = message.result
+                    stats.update_worker_stats(sender, message.result.statistics)
+
+                    if message.result.HasField("err"):
+                        logging.info(f"{sender} finished erroneously with `{message.result.err}`.")
+
+                    if message.result.HasField("ok"):
+                        ok = message.result.ok
+                        logging.info(
+                            f"{sender} finished cleanly with {pb.SmtDWorkerResult.Name(ok)}."
+                        )
+
+                        num_cleanly_finished = sum(
+                            1
+                            for _ in interface.workers
+                            if (_ in cm.worker_to_result) and cm.worker_to_result[_].HasField("ok")
+                        )
+                        if args.disable_early_stopping and num_cleanly_finished < len(
+                            interface.workers
+                        ):
+                            pass
+                        elif winner := judge_potential_winner(sender, message.result, cm):
+                            winner_duration = time.time() - start_time
+                            break
+
+                    if len(cm.worker_to_result) == len(interface.workers):
+                        logging.info("All workers have finished but none are winners.")
+                        break
+
+    except TimeoutError as e:
+        logging.info(f"Broker timeout: caught TimeoutError {e}")
+        logging.info(f"Broker timeout: should only result at system timeout {req.timeout_secs}s")
+        # raise  # doesn't do anything, swallowed by finally-return
+
+    except Exception as e:
+        logging.exception(f"Clause broker failed in an unexpected way: {e}")
+        # raise  # doesn't do anything, swallowed by finally-return
+
+    finally:
+        SetupTeardownTimer.begin(SetupTeardownTimer.Phases.SCIENCE_TEARDOWN)
+        for ctrl in share_length_controllers.values():
+            ctrl.stop()
+
+        duration = time.time() - start_time
+        logging.info(f"Broker duration: {duration:.3f}sec.")
+
+        # send abort message here if/when that is implemented
+
+        stats.handle_user_stats({"share_length_controllers": share_length_controllers})
+        stats.print()
+        logging.info("Results:")
+        for s, r in cm.worker_to_result.items():
+            logging.info(f"\t{s} => {result_short_str(r)}")
+
+        logging.info(f"The winner is {winner} in {winner_duration:.3f} seconds.")
+        result = cm.worker_to_result[winner] if winner else None
+        write_cluster_result(cm.worker_to_result, interface, args)
+        return (winner, result, winner_duration) if winner else (None, None, -1)
diff --git a/src/smtd/broker/science/control_loops/UserControlLoop.py b/src/smtd/broker/science/control_loops/UserControlLoop.py
new file mode 100644
index 0000000..4137c91
--- /dev/null
+++ b/src/smtd/broker/science/control_loops/UserControlLoop.py
@@ -0,0 +1,44 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+import asyncio
+from abc import ABC, abstractmethod
+
+from smtd.broker.science.control_loops.signals import LowPassFilter
+
+
+class UserControlLoop(ABC):
+    def __init__(
+        self,
+        gain_kP: float,
+        target: float,
+        initial_output: int,
+        min_output: int,
+        max_output: int,
+        control_loop_frequency=100,  # hertz
+    ):
+        self.gain_kP = gain_kP
+        self.target = target
+        self.output = initial_output
+        self.min_output = min_output
+        self.max_output = max_output
+        self.control_loop_frequency = control_loop_frequency
+
+        self.lpf = LowPassFilter(K=0.1, assume_uniform_sampling=True, init_value=target)
+        self.last_total_cpu_time = 0
+        self.last_total_elapsed_time = 0
+        self.last_total_subtract_time = 0
+
+        self.output = max_output
+
+        self._task = asyncio.create_task(self._loop())
+
+    # @abstractmethod
+    def stop(self):
+        pass
+
+    # @abstractmethod
+    async def _loop(self):
+        pass
+
+    # @abstractmethod
+    def update_control_loop(self, _input):
+        pass
\ No newline at end of file
diff --git a/src/smtd/broker/science/statistics/AbstractStatsHandler.py b/src/smtd/broker/science/statistics/AbstractStatsHandler.py
index 47389cd..8996271 100644
--- a/src/smtd/broker/science/statistics/AbstractStatsHandler.py
+++ b/src/smtd/broker/science/statistics/AbstractStatsHandler.py
@@ -1,5 +1,5 @@
 import logging
-from abc import abstractmethod
+from abc import ABC, abstractmethod
 from typing import Dict
 
 import numpy as np
@@ -9,7 +9,7 @@
 from smtd.proto import service_api_pb2 as pb
 
 
-class AbstractStatsHandler:
+class AbstractStatsHandler(ABC):
     def incr(self, *args):
         d = self.broker_stats
         for arg in args[:-2]:
@@ -30,3 +30,7 @@ def update_distinct(self, sender, senders):
     @abstractmethod
     def print(self, f=None, _print=logging.info):
         pass
+
+    @abstractmethod
+    def handle_user_stats(self, _input):
+        pass
diff --git a/src/smtd/broker/science/statistics/AsciiTableStatsHandler.py b/src/smtd/broker/science/statistics/AsciiTableStatsHandler.py
index ab74867..4882762 100644
--- a/src/smtd/broker/science/statistics/AsciiTableStatsHandler.py
+++ b/src/smtd/broker/science/statistics/AsciiTableStatsHandler.py
@@ -339,3 +339,6 @@ def generate_elapsed_profiling_table(self):
             ]
 
         return table
+    
+    def handle_user_stats(self, _input):
+        pass
diff --git a/src/smtd/broker/science/statistics/UserStatsHandler.py b/src/smtd/broker/science/statistics/UserStatsHandler.py
new file mode 100644
index 0000000..f94f11c
--- /dev/null
+++ b/src/smtd/broker/science/statistics/UserStatsHandler.py
@@ -0,0 +1,7 @@
+from abc import abstractmethod
+from smtd.broker.science.statistics.AsciiTableStatsHandler import AsciiTableStatsHandler
+
+class UserStatsHandler(AsciiTableStatsHandler):
+    @abstractmethod
+    def handle_user_stats(self, _input):
+        pass
\ No newline at end of file
diff --git a/src/smtd/broker/systems/communication/connection_lifecycle.py b/src/smtd/broker/systems/communication/connection_lifecycle.py
index 5904542..45cc6a7 100644
--- a/src/smtd/broker/systems/communication/connection_lifecycle.py
+++ b/src/smtd/broker/systems/communication/connection_lifecycle.py
@@ -109,7 +109,7 @@ async def _export_loop(
         # async with asyncio.timeout(connection_timeout_secs):  # no idea how this will execute... but its less scary
         #     await stream.done_writing()
         await asyncio.shield(
-            asyncio.wait_for(  # this better eventually exit or we're in big trouble !!!
+            asyncio.wait_for(  # this better eventually exit or we're in big trouble!
                 stream.done_writing(), connection_timeout_secs
             )
         )
diff --git a/src/smtd/proto/custom_proto.proto b/src/smtd/proto/custom_proto.proto
new file mode 100644
index 0000000..973e95f
--- /dev/null
+++ b/src/smtd/proto/custom_proto.proto
@@ -0,0 +1,6 @@
+syntax = "proto3";
+          package SmtD;
+
+          message SmtDWrapperCustomOptions {
+            uint32 custom = 1;
+          }
diff --git a/src/smtd/proto/service_api.proto b/src/smtd/proto/service_api.proto
index 18f08c8..f13be1e 100644
--- a/src/smtd/proto/service_api.proto
+++ b/src/smtd/proto/service_api.proto
@@ -1,6 +1,7 @@
 syntax = "proto3";
 import "google/protobuf/timestamp.proto";
 import "smtd/proto/semi_structured_api.proto";
+import "smtd/proto/custom_proto.proto";
 
 package SmtD;
 
@@ -31,7 +32,7 @@ message SmtDSmtExpression {
     string smtlib = 1;
     string s3url = 3;
     string filepath = 4;
-    SmtSemiStructuredExpression soapi = 2;
+    SmtSemiStructuredExpression ssapi = 2;
   }
 }
 
@@ -149,6 +150,8 @@ message SmtDStatus {
 
   optional SmtDStatusSysinfo linux_sysinfo = 14;
   optional SmtDStatusRusage linux_rusage = 15;
+
+  SmtDWrapperCustomOptions custom_fields = 23;
 }
 
 message SmtDStatusSysinfo {
diff --git a/src/smtd/workers/CMakeLists.txt b/src/smtd/workers/CMakeLists.txt
index b7b236b..0f0fee1 100644
--- a/src/smtd/workers/CMakeLists.txt
+++ b/src/smtd/workers/CMakeLists.txt
@@ -90,6 +90,7 @@ endif ()
 # must be explicitly listed for CMake.. easiest just to hardcode
 set(proto_names
         "service_api"
+        "custom_proto"
         "semi_structured_api"
 )
 
diff --git a/src/smtd/workers/src/science/CustomHeuristics.cpp b/src/smtd/workers/src/science/CustomHeuristics.cpp
new file mode 100644
index 0000000..219630e
--- /dev/null
+++ b/src/smtd/workers/src/science/CustomHeuristics.cpp
@@ -0,0 +1,6 @@
+#include <iostream>
+          #include "CustomHeuristics.h"
+
+          void CustomHeuristics::dummy(SmtD::SmtDStatus &d_stats, std::optional<std::reference_wrapper<const cvc5::Term>> lemma, SemiStructuredContext &ssctx, SmtDWorkerInterface &d_interface) {
+              return;
+          }
diff --git a/src/smtd/workers/src/science/CustomHeuristics.h b/src/smtd/workers/src/science/CustomHeuristics.h
new file mode 100644
index 0000000..b726217
--- /dev/null
+++ b/src/smtd/workers/src/science/CustomHeuristics.h
@@ -0,0 +1,8 @@
+#ifndef CVC5__CUSTOM_HEURISTICS_H
+          #define CVC5__CUSTOM_HEURISTICS_H
+          #include "UserHeuristics.h"
+          class CustomHeuristics : public UserHeuristics {
+          public:
+              void dummy(SmtD::SmtDStatus &d_stats, std::optional<std::reference_wrapper<const cvc5::Term>> lemma, SemiStructuredContext &ssctx, SmtDWorkerInterface &d_interface) override;
+              };
+          #endif 
\ No newline at end of file
diff --git a/src/smtd/workers/src/science/LemmaTransceiver.cpp b/src/smtd/workers/src/science/LemmaTransceiver.cpp
index 4e400b6..5c2fcce 100644
--- a/src/smtd/workers/src/science/LemmaTransceiver.cpp
+++ b/src/smtd/workers/src/science/LemmaTransceiver.cpp
@@ -13,11 +13,16 @@
  * Lemma loader for cvc5.
  */
 #include <iostream>
+#include <dlfcn.h>
 #include <sstream>
 
 #include "LemmaTransceiver.h"
 #include "LinuxStatistics.h"
 #include "MeasureClauseSize.h"
+#include "CustomHeuristics.h"
+
+typedef UserHeuristics* (*CreateFunc)();
+typedef void (*DestroyFunc)(UserHeuristics*);
 
 
 class SmtDWorkerInterface;
@@ -42,12 +47,15 @@ namespace cvc5 {
                 SmtDWorkerInterface &interface
         ) : cvc5::Plugin(tm), d_solver(s), d_symman(sm),
             d_ip(new parser::InputParser(s, sm)), d_interface(interface),
-            ssctx(*d_ip, d_interface.workerID(), d_options) {
+            ssctx(*d_ip, d_interface.workerID(), d_options),
+            uh(std::make_unique<CustomHeuristics>()) {
             d_options = defaultOptions();
             setStartTime();
         }
 
-        LemmaTransceiver::~LemmaTransceiver() { delete d_ip; }
+        LemmaTransceiver::~LemmaTransceiver() { 
+            delete d_ip;
+        }
 
         void LemmaTransceiver::setStartTime() {
             d_interface.feedWatchdog();
@@ -91,6 +99,7 @@ namespace cvc5 {
             if (d_options.worker_debug()) {
                 std::cout << "Imported " << adapt_msgs.size() << " adapts." << std::endl;
                 std::cout << "Imported " << lemma_msgs.size() << " lemmas." << std::endl;
+                std::cout << "Imported " << def_msgs.size() << " defs." << std::endl;
             }
 
             for (const auto &o: adapt_msgs) {
@@ -104,12 +113,12 @@ namespace cvc5 {
                 bool should_not_filter = false;
                 assert(l.formula_id() == 0); // multi-solving is not supported yet.
 
-                if (!l.expr().has_soapi()) {
+                if (!l.expr().has_ssapi()) {
                     std::cerr << "Received unsupported lemma format: " << l.DebugString() << std::endl;
                     continue;
                 }
 
-                const auto maybe_lemma = ssctx.try_proto_to_term(l.expr().soapi());
+                const auto maybe_lemma = ssctx.try_proto_to_term(l.expr().ssapi());
                 if (!maybe_lemma.has_value()) {
                     continue; // parsing/term construction failed
                 } // else {
@@ -168,6 +177,14 @@ namespace cvc5 {
             d_total_plugin_export_time += PLUGIN_NOTIFY_END_TIME - PLUGIN_NOTIFY_START_TIME;
         }
 
+        // TODO: Handle optional lemma in a better way (right now, it is passed by value)
+        //       It would be better to do an optional reference, but that seems thorny in C++...
+        void LemmaTransceiver::dummyWrapper(std::optional<std::reference_wrapper<const cvc5::Term>> lemma) {
+            if (uh) {
+                uh->dummy(d_stats, lemma, ssctx, d_interface);
+            } 
+        }
+
         void LemmaTransceiver::notifyLogic(const Term &lemma, const bool is_theory) {
             if (is_theory) { incr_stat(num_theory_lemmas_exported, 1); }
             if (!is_theory) { incr_stat(num_sat_clauses_exported, 1); }
@@ -175,6 +192,13 @@ namespace cvc5 {
             // 64 is maximum breadth, beyond which we take random-ish sampling of term children
             const auto HEURISTIC_START_TIME = high_resolution_clock::now();
             const auto heuristic_time_percent = 100ull * d_export_heuristic_time.count() / (HEURISTIC_START_TIME - d_start_wall_clock_time).count();
+
+            if (heuristic_time_percent < 5) {
+                dummyWrapper(lemma);
+            }
+
+            //std::cout << "Got here! Past dummyWrapper" << std::endl;
+
             const auto HEURISTIC_END_TIME = high_resolution_clock::now();
             d_export_heuristic_time += HEURISTIC_END_TIME - HEURISTIC_START_TIME;
 
@@ -188,8 +212,12 @@ namespace cvc5 {
             const auto FILTER1_END_TIME = high_resolution_clock::now();
             d_export_filter_time += FILTER1_END_TIME - FILTER1_START_TIME;
 
+            //std::cout << "Got here! 1" << std::endl;
+
             if (numLiterals > d_options.share_length()) return;
 
+            //std::cout << "Got here! 1.5" << std::endl;
+
 //          const auto SIMPLIFY_START_TIME = high_resolution_clock::now();
 //          const auto SIMPLIFY_END_TIME = high_resolution_clock::now();
 //          d_export_simplify_time += SIMPLIFY_END_TIME - SIMPLIFY_START_TIME;
@@ -201,19 +229,26 @@ namespace cvc5 {
                 has_been_seen = !seen.insert(getChildIDs(lemma)).second;
                 if (!has_been_seen) prevent_gc.insert(lemma);
             }
+
+            //std::cout << "Got here! 2" << std::endl;
+
             // todo: insert other filtering strategies here.
             // ^^^ FILTERING ONLY ^^^
             const auto FILTER2_END_TIME = high_resolution_clock::now();
             d_export_filter_time += FILTER2_END_TIME - FILTER2_START_TIME;
 
+            //std::cout << "Got here! 3" << std::endl;
+
             if (has_been_seen) {
                 if (is_theory) { incr_stat(num_theory_lemmas_export_filtered, 1); }
                 else { incr_stat(num_sat_clauses_export_filtered, 1); }
                 return;
             }
 
+            //std::cout << "Got here! 4" << std::endl;
+
             SmtD::SmtDSmtLemma pb_lemma;
-            *pb_lemma.mutable_expr()->mutable_soapi() = ssctx.term_to_proto(
+            *pb_lemma.mutable_expr()->mutable_ssapi() = ssctx.term_to_proto(
                     lemma, [&](const SmtD::SmtSemiStructuredDefinition &msg) { return d_interface.defineAtom(msg); }
             );
             pb_lemma.mutable_metadata()->set_length(numLiterals);
@@ -225,6 +260,8 @@ namespace cvc5 {
                 std::cerr << "WARNING: exportImmediate failed!" << std::endl;
             }
 
+            //std::cout << "Got here! Right before exporting" << std::endl;
+
             if (d_options.worker_debug()) {
                 std::cout << to_ms(high_resolution_clock::now() - d_start_wall_clock_time) << "ms -- Export: "
                           << (is_theory ? 't' : 's') << ' '
@@ -245,6 +282,8 @@ namespace cvc5 {
                         d_stats, d_start_ru_utime_ms, d_start_ru_stime_ms
                 )) /* copy was successful, no-op */;
                 else d_stats.clear_linux_rusage();
+                
+                dummyWrapper(std::nullopt);
 
                 // timing information should be copied (and rounded/truncated down) at the last moment
 #define cp(__FIELD__)        (d_stats.set_##__FIELD__##_ms( to_ms( d_##__FIELD__ ) ))
diff --git a/src/smtd/workers/src/science/LemmaTransceiver.h b/src/smtd/workers/src/science/LemmaTransceiver.h
index f4b6469..da8e0bb 100644
--- a/src/smtd/workers/src/science/LemmaTransceiver.h
+++ b/src/smtd/workers/src/science/LemmaTransceiver.h
@@ -24,6 +24,7 @@
 #include <cvc5/cvc5_parser.h>
 #include "../SmtDWorkerInterface.h"
 #include "SemiStructuredContext.h"
+#include "UserHeuristics.h"
 
 
 namespace cvc5::main {
@@ -44,6 +45,8 @@ namespace cvc5::main {
 
         void setStartTime();
 
+        void dummyWrapper(std::optional<std::reference_wrapper<const cvc5::Term>> lemma);
+
         /** Returns a list of formulas to be sent as lemmas to the internal worker */
         std::vector<Term> check() override;
 
@@ -90,6 +93,7 @@ namespace cvc5::main {
         SmtD::SmtDWrapperOptions d_options;
         SmtD::SmtDHeartbeat d_hb;
         SmtD::SmtDStatus &d_stats = *d_hb.mutable_still_running();
+        std::unique_ptr<UserHeuristics> uh;
 
         // Lemma Loader
         std::chrono::nanoseconds
diff --git a/src/smtd/workers/src/science/SemiStructuredContext.cpp b/src/smtd/workers/src/science/SemiStructuredContext.cpp
index d429821..5660b4a 100644
--- a/src/smtd/workers/src/science/SemiStructuredContext.cpp
+++ b/src/smtd/workers/src/science/SemiStructuredContext.cpp
@@ -20,7 +20,7 @@ std::optional<cvc5::Term> SemiStructuredContext::try_proto_to_term(const SmtD::S
         const auto iter = uuid_to_term.find(m.uuid());
         if (iter != uuid_to_term.end()) return iter->second;
         else {
-            std::cerr << "SOAPI ERROR: Received undefined UUID " << m.uuid().ShortDebugString() << ". Dropping lemma." << std::endl;
+            std::cerr << "SSAPI ERROR: Received undefined UUID " << m.uuid().ShortDebugString() << ". Dropping lemma." << std::endl;
             return std::nullopt;
         }
 
@@ -90,14 +90,14 @@ SmtD::SmtSemiStructuredExpression SemiStructuredContext::term_to_proto(const cvc
         // AND ANYWHERE ELSE WE MIGHT CALL toString ON A TERM (see Heuristics.cpp, etc.)
         const auto len = def.str().length();
         if (len > options.ssctx_atom_size_limit()) {
-            std::cerr << "SOAPI ERROR: Dropping " << len << " byte atom, which exceeds export size limit of " << options.ssctx_atom_size_limit() << " bytes." << std::endl;
+            std::cerr << "SSAPI ERROR: Dropping " << len << " byte atom, which exceeds export size limit of " << options.ssctx_atom_size_limit() << " bytes." << std::endl;
             oversized_atoms_dropped++;
             // skip next case that calls `exportDefinition()`
             // other workers should handle dropped and missing atoms gracefully. nothing here to do
             // todo: maybe some sort of "unsound cache" which only stores the hash?
             // that way we can still run heuristics... maybe all the workers are producing the exact same massive atoms? idk
         } else if (exportDefinition(def)) {
-            std::cerr << "SOAPI ERROR: Failed to export definition: " << def.DebugString() << std::endl;
+            std::cerr << "SSAPI ERROR: Failed to export definition: " << def.DebugString() << std::endl;
         }
 
         *ret.mutable_uuid() = def.new_uuid();
@@ -133,7 +133,7 @@ void SemiStructuredContext::record_definition(const SmtD::SmtSemiStructuredDefin
 
             } else {
                 // it's okay, this happens when the original term had a skolem and the parser failed
-//                std::cerr << "SOAPI ERROR: Could not remap term from UUID " << def.old_uuid().ShortDebugString() << " to " << def.new_uuid().ShortDebugString() << " since neither of the UUIDs are known." << std::endl;
+//                std::cerr << "SSAPI ERROR: Could not remap term from UUID " << def.old_uuid().ShortDebugString() << " to " << def.new_uuid().ShortDebugString() << " since neither of the UUIDs are known." << std::endl;
             }
         }
 
@@ -154,7 +154,7 @@ void SemiStructuredContext::record_definition(const SmtD::SmtSemiStructuredDefin
             success = true;
         } catch (const cvc5::CVC5ApiException &err) {
             // it probably contained a skolem
-            std::cerr << "SOAPI ERROR: `" << err << "` on string `" << def.str() << "`." << std::endl;
+            std::cerr << "SSAPI ERROR: `" << err << "` on string `" << def.str() << "`." << std::endl;
             success = false;
         }
         const auto PARSE_END_TIME = std::chrono::high_resolution_clock::now();
@@ -167,15 +167,14 @@ void SemiStructuredContext::record_definition(const SmtD::SmtSemiStructuredDefin
         const auto SIMPLIFY_END_TIME = std::chrono::high_resolution_clock::now();
         import_simplify_time += SIMPLIFY_END_TIME - SIMPLIFY_START_TIME;
 
-
         const auto booliter = uuid_to_term.insert({def.new_uuid(), simple_term});
         if (!booliter.second) {
-            std::cerr << "SOAPI ERROR: uuid " << def.new_uuid().ShortDebugString() << " cannot be reassigned\n" <<
+            std::cerr << "SSAPI ERROR: uuid " << def.new_uuid().ShortDebugString() << " cannot be reassigned\n" <<
                       "from: `" << booliter.first->second << "`\n" <<
                       "to: `" << simple_term << "`\n" <<
-                      "This is might be unsound. Exiting!" << std::endl;
+                      "This might be unsound. Exiting!" << std::endl;
 
-            throw std::logic_error("SOAPI received two different terms for the same UUID. This might be unsound.");
+            throw std::logic_error("SSAPI received two different terms for the same UUID. This might be unsound.");
         }
         term_to_uuid[simple_term] = def.new_uuid();
     }
diff --git a/src/smtd/workers/src/science/UserHeuristics.h b/src/smtd/workers/src/science/UserHeuristics.h
new file mode 100644
index 0000000..a4d265a
--- /dev/null
+++ b/src/smtd/workers/src/science/UserHeuristics.h
@@ -0,0 +1,15 @@
+#ifndef USER_HEURISTICS_H
+#define USER_HEURISTICS_H
+
+// #include "smtd/proto/service_api.pb.h"
+// #include <cvc5/cvc5.h>
+#include "SemiStructuredContext.h"
+#include "../SmtDWorkerInterface.h"
+
+class UserHeuristics {
+    public:
+        virtual ~UserHeuristics() = default;
+        virtual void dummy(SmtD::SmtDStatus &d_stats, std::optional<std::reference_wrapper<const cvc5::Term>> lemma, SemiStructuredContext &ssctx, SmtDWorkerInterface &d_interface) = 0;
+};
+
+#endif
\ No newline at end of file
diff --git a/src/smtd/workers/src/systems/server/SmtDWorkerGrpcQueueImpl.cpp b/src/smtd/workers/src/systems/server/SmtDWorkerGrpcQueueImpl.cpp
index 8d253d6..7954666 100644
--- a/src/smtd/workers/src/systems/server/SmtDWorkerGrpcQueueImpl.cpp
+++ b/src/smtd/workers/src/systems/server/SmtDWorkerGrpcQueueImpl.cpp
@@ -224,6 +224,7 @@ uint16_t SmtDWorkerGrpcQueueImpl::workerID() {
 }
 
 int SmtDWorkerGrpcQueueImpl::defineAtom(const SmtD::SmtSemiStructuredDefinition &d) {
+    std::cerr << "DEFINING ATOM " << d.new_uuid().ShortDebugString() << std::endl;
     SmtD::FromSmtDMessage msg;
     *msg.mutable_define() = d;
     bool success = _message_export_q.enqueue(msg);