diff --git a/src/api/Interpret.cc b/src/api/Interpret.cc
index 99366d4ea..cd5e32e35 100644
--- a/src/api/Interpret.cc
+++ b/src/api/Interpret.cc
@@ -1284,22 +1284,7 @@ void Interpret::getProof()
 
 void Interpret::getUnsatCore() {
     auto const unsatCore = main_solver->getUnsatCore();
-    std::cout << "(\n";
-    auto const & termNames = main_solver->getTermNames();
-    if (not config.print_cores_full()) {
-        // this is the default: we care only about ':named' terms and their names
-        for (PTRef fla : unsatCore->getNamedTerms()) {
-            assert(termNames.contains(fla));
-            auto const & name = termNames.nameForTerm(fla);
-            std::cout << name << '\n';
-        }
-    } else {
-        // we explicitly asked to include all terms and to ignore ':named' terms at all
-        for (PTRef fla : unsatCore->getTerms()) {
-            std::cout << logic->printTerm(fla) << '\n';
-        }
-    }
-    std::cout << ')' << std::endl;
+    unsatCore->print();
 }
 
 void Interpret::getInterpolants(const ASTNode& n)
diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc
index b5b33795b..44b6bb28b 100644
--- a/src/api/MainSolver.cc
+++ b/src/api/MainSolver.cc
@@ -272,8 +272,7 @@ std::unique_ptr<UnsatCore> MainSolver::getUnsatCore() const {
     if (not config.produce_unsat_cores()) { throw ApiException("Producing unsat cores is not enabled"); }
     if (status != s_False) { throw ApiException("Unsat core cannot be extracted if solver is not in UNSAT state"); }
 
-    auto & proof = smt_solver->getResolutionProof();
-    UnsatCoreBuilder unsatCoreBuilder{config, logic, proof, pmanager, termNames};
+    UnsatCoreBuilder unsatCoreBuilder{*this};
 
     return unsatCoreBuilder.build();
 }
diff --git a/src/api/MainSolver.h b/src/api/MainSolver.h
index c77ab118f..01fc6ad37 100644
--- a/src/api/MainSolver.h
+++ b/src/api/MainSolver.h
@@ -138,6 +138,8 @@ class MainSolver {
     static std::unique_ptr<Theory> createTheory(Logic & logic, SMTConfig & config);
 
 protected:
+    friend class UnsatCoreBuilderBase;
+
     using FrameId = uint32_t;
 
     struct PushFrame {
diff --git a/src/common/TermNames.h b/src/common/TermNames.h
index fd6fe3e89..4f4a0e0f0 100644
--- a/src/common/TermNames.h
+++ b/src/common/TermNames.h
@@ -2,9 +2,12 @@
 #define OPENSMT_TERMNAMES_H
 
 #include "ScopedVector.h"
+#include "TypeUtils.h"
 
+#include <options/SMTConfig.h>
 #include <pterms/PTRef.h>
 
+#include <algorithm>
 #include <optional>
 #include <string>
 #include <type_traits>
diff --git a/src/unsatcores/CMakeLists.txt b/src/unsatcores/CMakeLists.txt
index ad6a95174..28165eb55 100644
--- a/src/unsatcores/CMakeLists.txt
+++ b/src/unsatcores/CMakeLists.txt
@@ -4,6 +4,7 @@ target_sources(unsatcores
 PUBLIC
     "${CMAKE_CURRENT_SOURCE_DIR}/UnsatCore.h"
 PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/UnsatCore.cc"
     "${CMAKE_CURRENT_SOURCE_DIR}/UnsatCoreBuilder.h"
     "${CMAKE_CURRENT_SOURCE_DIR}/UnsatCoreBuilder.cc"
 )
diff --git a/src/unsatcores/UnsatCore.cc b/src/unsatcores/UnsatCore.cc
new file mode 100644
index 000000000..fc90fe394
--- /dev/null
+++ b/src/unsatcores/UnsatCore.cc
@@ -0,0 +1,44 @@
+#include "UnsatCore.h"
+
+#include <common/TermNames.h>
+#include <logics/Logic.h>
+
+#include <iostream>
+
+namespace opensmt {
+
+void UnsatCore::print() const {
+    print(std::cout);
+}
+
+void UnsatCore::print(std::ostream & os) const {
+    printBegin(os);
+    printBody(os);
+    printEnd(os);
+}
+
+void UnsatCore::printBegin(std::ostream & os) const {
+    os << "(\n";
+}
+
+void UnsatCore::printBody(std::ostream & os) const {
+    for (PTRef term : getTerms()) {
+        printTerm(os, term);
+        os << '\n';
+    }
+}
+
+void UnsatCore::printEnd(std::ostream & os) const {
+    os << ')' << std::endl;
+}
+
+void NamedUnsatCore::printTerm(std::ostream & os, PTRef term) const {
+    assert(termNames.contains(term));
+    os << termNames.nameForTerm(term);
+}
+
+void FullUnsatCore::printTerm(std::ostream & os, PTRef term) const {
+    os << logic.printTerm(term);
+}
+
+} // namespace opensmt
diff --git a/src/unsatcores/UnsatCore.h b/src/unsatcores/UnsatCore.h
index 1ae8229e6..168365ddd 100644
--- a/src/unsatcores/UnsatCore.h
+++ b/src/unsatcores/UnsatCore.h
@@ -4,25 +4,77 @@
 #include <minisat/mtl/Vec.h>
 #include <pterms/PTRef.h>
 
+#include <iosfwd>
+
 namespace opensmt {
 
+class Logic;
+class TermNames;
+
 class UnsatCore {
 public:
+    virtual ~UnsatCore() = default;
+
+    virtual vec<PTRef> const & getTerms() const = 0;
+
+    void print() const;
+    void print(std::ostream &) const;
+
+protected:
+    UnsatCore() = default;
+
+    void printBegin(std::ostream &) const;
+    void printBody(std::ostream &) const;
+    void printEnd(std::ostream &) const;
+
+    virtual void printTerm(std::ostream &, PTRef) const = 0;
+};
+
+class NamedUnsatCore : public UnsatCore {
+public:
+    vec<PTRef> const & getTerms() const override { return namedTerms; }
+
+    vec<PTRef> const & getHiddenTerms() const { return hiddenTerms; }
+
+protected:
     friend class UnsatCoreBuilder;
 
-    vec<PTRef> const & getTerms() const { return terms; }
-    vec<PTRef> const & getNamedTerms() const { return namedTerms; }
+    inline NamedUnsatCore(TermNames const &, vec<PTRef> && namedTerms_, vec<PTRef> && hiddenTerms_);
+
+    void printTerm(std::ostream &, PTRef) const override;
+
+    TermNames const & termNames;
+
+    vec<PTRef> namedTerms;
+    vec<PTRef> hiddenTerms;
+};
+
+class FullUnsatCore : public UnsatCore {
+public:
+    vec<PTRef> const & getTerms() const override { return terms; }
 
 protected:
-    inline UnsatCore(vec<PTRef> && terms_, vec<PTRef> && namedTerms_);
+    friend class UnsatCoreBuilder;
+
+    inline FullUnsatCore(Logic const &, vec<PTRef> && terms_);
+
+    void printTerm(std::ostream &, PTRef) const override;
+
+    Logic const & logic;
 
     vec<PTRef> terms;
-    vec<PTRef> namedTerms;
 };
 
-UnsatCore::UnsatCore(vec<PTRef> && terms_, vec<PTRef> && namedTerms_)
-    : terms{std::move(terms_)},
-      namedTerms{std::move(namedTerms_)} {
+////////////////////////////////////////////////////////////////////////////////
+
+NamedUnsatCore::NamedUnsatCore(TermNames const & termNames_, vec<PTRef> && namedTerms_, vec<PTRef> && hiddenTerms_)
+    : termNames{termNames_},
+      namedTerms{std::move(namedTerms_)},
+      hiddenTerms{std::move(hiddenTerms_)} {
+    assert(namedTerms.size() > 0 || hiddenTerms.size() > 0);
+}
+
+FullUnsatCore::FullUnsatCore(Logic const & logic_, vec<PTRef> && terms_) : logic{logic_}, terms{std::move(terms_)} {
     assert(terms.size() > 0);
 }
 
diff --git a/src/unsatcores/UnsatCoreBuilder.cc b/src/unsatcores/UnsatCoreBuilder.cc
index d87da8bee..d74c660d4 100644
--- a/src/unsatcores/UnsatCoreBuilder.cc
+++ b/src/unsatcores/UnsatCoreBuilder.cc
@@ -16,6 +16,13 @@ namespace opensmt {
 
 using Partitions = ipartitions_t;
 
+UnsatCoreBuilderBase::UnsatCoreBuilderBase(MainSolver const & solver_)
+    : solver{solver_},
+      config{solver_.config},
+      logic{solver_.logic},
+      proof{solver_.smt_solver->getResolutionProof()},
+      partitionManager{solver_.pmanager} {}
+
 std::unique_ptr<UnsatCore> UnsatCoreBuilder::build() {
     buildBody();
     return buildReturn();
@@ -23,15 +30,20 @@ std::unique_ptr<UnsatCore> UnsatCoreBuilder::build() {
 
 void UnsatCoreBuilder::buildBody() {
     computeClauses();
-    computeTerms();
-    computeNamedTerms();
+    mapClausesToTerms();
+
+    if (not config.print_cores_full()) { partitionNamedTerms(); }
 
     if (config.minimal_unsat_cores()) { minimize(); }
 }
 
 std::unique_ptr<UnsatCore> UnsatCoreBuilder::buildReturn() {
-    // Not using `make_unique` because only UnsatCoreBuilder is a friend of UnsatCore
-    return std::unique_ptr<UnsatCore>{new UnsatCore{std::move(terms), std::move(namedTerms)}};
+    // Not using `make_unique` because only UnsatCoreBuilder is a friend of *UnsatCore
+
+    if (config.print_cores_full()) { return std::unique_ptr<UnsatCore>{new FullUnsatCore{logic, std::move(allTerms)}}; }
+
+    return std::unique_ptr<UnsatCore>{
+        new NamedUnsatCore{solver.getTermNames(), std::move(namedTerms), std::move(hiddenTerms)}};
 }
 
 void UnsatCoreBuilder::computeClauses() {
@@ -60,9 +72,9 @@ void UnsatCoreBuilder::computeClauses() {
     }
 }
 
-void UnsatCoreBuilder::computeTerms() {
+void UnsatCoreBuilder::mapClausesToTerms() {
     assert(clauses.size() > 0);
-    assert(terms.size() == 0);
+    assert(allTerms.size() == 0);
 
     Partitions partitions;
     for (CRef cref : clauses) {
@@ -70,30 +82,53 @@ void UnsatCoreBuilder::computeTerms() {
         orbit(partitions, partitions, partition);
     }
 
-    terms = partitionManager.getPartitions(partitions);
+    allTerms = partitionManager.getPartitions(partitions);
 }
 
-void UnsatCoreBuilder::computeNamedTerms() {
-    assert(terms.size() > 0);
+void UnsatCoreBuilder::partitionNamedTerms() {
+    assert(allTerms.size() > 0);
     namedTerms.clear();
-    namedTermsIdxs.clear();
+    hiddenTerms.clear();
 
-    if (config.print_cores_full()) return;
+    auto const & termNames = solver.getTermNames();
+    if (termNames.empty()) {
+        hiddenTerms = std::move(allTerms);
+        return;
+    }
 
-    if (termNames.empty()) return;
+    for (PTRef term : allTerms) {
+        if (termNames.contains(term)) {
+            namedTerms.push(term);
+        } else {
+            hiddenTerms.push(term);
+        }
+    }
 
-    size_t const termsSize = terms.size();
-    for (size_t idx = 0; idx < termsSize; ++idx) {
-        PTRef term = terms[idx];
-        if (not termNames.contains(term)) { continue; }
-        namedTerms.push(term);
-        namedTermsIdxs.push_back(idx);
+    allTerms.clear();
+}
+
+void UnsatCoreBuilder::minimize() {
+    if (config.print_cores_full()) {
+        allTerms = Minimize{*this, std::move(allTerms)}.perform();
+        return;
     }
+
+    namedTerms = Minimize{*this, std::move(namedTerms), hiddenTerms}.perform();
 }
 
-SMTConfig UnsatCoreBuilder::makeSmtSolverConfig() const {
-    assert(config.minimal_unsat_cores());
+////////////////////////////////////////////////////////////////////////////////
+
+UnsatCoreBuilder::Minimize::Minimize(UnsatCoreBuilder & builder_, vec<PTRef> targetTerms_,
+                                     vec<PTRef> const & backgroundTerms_)
+    : builder{builder_},
+      targetTerms{std::move(targetTerms_)},
+      backgroundTerms{backgroundTerms_} {
+    assert(builder.config.minimal_unsat_cores());
+}
 
+UnsatCoreBuilder::Minimize::~Minimize() {}
+
+SMTConfig UnsatCoreBuilder::Minimize::makeSmtSolverConfig() const {
     SMTConfig newConfig;
     assert(newConfig.isIncremental());
     assert(newConfig.verbosity() == 0);
@@ -110,97 +145,56 @@ SMTConfig UnsatCoreBuilder::makeSmtSolverConfig() const {
     return newConfig;
 }
 
-std::unique_ptr<UnsatCoreBuilder::SMTSolver> UnsatCoreBuilder::newSmtSolver(SMTConfig & newConfig) const {
-    assert(config.minimal_unsat_cores());
-
-    return std::make_unique<SMTSolver>(logic, newConfig, "unsat core solver");
-}
-
-void UnsatCoreBuilder::minimize() {
-    minimizeInit();
-    minimizeAlg();
-    minimizeFinish();
-}
-
-void UnsatCoreBuilder::minimizeInit() {
-    assert(terms.size() > 0);
-    assert(terms.size() >= namedTerms.size());
-    assert(size_t(namedTerms.size()) == namedTermsIdxs.size());
+std::unique_ptr<UnsatCoreBuilder::Minimize::InternalSMTSolver>
+UnsatCoreBuilder::Minimize::newSmtSolver(SMTConfig & newConfig) const {
+    return std::make_unique<InternalSMTSolver>(builder.logic, newConfig, "min unsat core solver");
 }
 
-void UnsatCoreBuilder::minimizeAlgNaive() {
-    bool const fullCore = config.print_cores_full();
+vec<PTRef> UnsatCoreBuilder::Minimize::perform() && {
+    if (targetTerms.size() == 0) { return std::move(targetTerms); }
 
-    // this algorithm will minimize the contents of the `namedTerms` vector
+    SMTConfig smtSolverConfig = makeSmtSolverConfig();
+    std::unique_ptr<InternalSMTSolver> smtSolverPtr = newSmtSolver(smtSolverConfig);
 
-    if (fullCore) {
-        // special case: we don't care about named terms, hence we must minimize everything
-        assert(namedTerms.size() == 0);
-        std::swap(terms, namedTerms);
-        assert(namedTerms.size() > 0);
-    } else if (namedTerms.size() == 0) {
-        return;
-    }
+    return performNaive(*smtSolverPtr);
+}
 
-    SMTConfig smtSolverConfig = makeSmtSolverConfig();
-    std::unique_ptr<SMTSolver> smtSolverPtr = newSmtSolver(smtSolverConfig);
-
-    decltype(terms) newTerms;
-    if (not fullCore) {
-        // the default: we focus on named terms -> we must distinguish between `namedTerms` and the others in `terms`
-        auto const namedTermsIdxsEnd = namedTermsIdxs.end();
-        auto const isNamedTerm = [namedTermsIdxsEnd](size_t idx, auto namedTermsIdxsIt) {
-            if (namedTermsIdxsIt == namedTermsIdxsEnd) { return false; }
-            assert(idx <= *namedTermsIdxsIt);
-            return (idx == *namedTermsIdxsIt);
-        };
-
-        size_t const termsSize = terms.size();
-        for (auto [idx, namedTermsIdxsIt] = std::tuple{size_t{0}, namedTermsIdxs.begin()}; idx < termsSize; ++idx) {
-            if (isNamedTerm(idx, namedTermsIdxsIt)) {
-                ++namedTermsIdxsIt;
-                continue;
-            }
-            // the term that we do not care about -> can be hard-asserted
-            PTRef term = terms[idx];
-            smtSolverPtr->insertFormula(term);
-            newTerms.push(term);
-        }
+vec<PTRef> UnsatCoreBuilder::Minimize::performNaive(InternalSMTSolver & smtSolver) {
+    for (PTRef term : backgroundTerms) {
+        // the term that we do not care about eliminating -> can be hard-asserted
+        smtSolver.insertFormula(term);
     }
 
-    // minimize the contents of the `namedTerms` vector (given the already asserted hard constraints)
+    // minimize the contents of `targetTerms` (given the already hard-asserted constraints)
 
-    decltype(namedTerms) newNamedTerms;
-    size_t const namedTermsSize = namedTerms.size();
-    for (size_t namedIdx = 0; namedIdx < namedTermsSize; ++namedIdx) {
-        smtSolverPtr->push();
+    decltype(targetTerms) newTargetTerms;
+    size_t const targetTermsSize = targetTerms.size();
+    for (size_t idx = 0; idx < targetTermsSize; ++idx) {
+        smtSolver.push();
 
-        // try to ignore namedTerms[namedIdx]
+        // try to ignore targetTerms[idx]
 
-        for (size_t keptNamedIdx = namedIdx + 1; keptNamedIdx < namedTermsSize; ++keptNamedIdx) {
-            PTRef term = namedTerms[keptNamedIdx];
-            smtSolverPtr->insertFormula(term);
+        for (size_t keptIdx = idx + 1; keptIdx < targetTermsSize; ++keptIdx) {
+            PTRef term = targetTerms[keptIdx];
+            smtSolver.insertFormula(term);
         }
 
-        sstat const res = smtSolverPtr->check();
+        sstat const res = smtSolver.check();
         assert(res == s_True || res == s_False);
         bool const isRedundant = (res == s_False);
 
-        smtSolverPtr->pop();
+        smtSolver.pop();
 
         if (isRedundant) continue;
 
-        // namedTerms[namedIdx] is not redundant - include it
+        // targetTerms[idx] is not redundant - include it
 
-        PTRef term = namedTerms[namedIdx];
-        smtSolverPtr->insertFormula(term);
-        newTerms.push(term);
-        if (not fullCore) { newNamedTerms.push(term); }
+        PTRef term = targetTerms[idx];
+        smtSolver.insertFormula(term); // can already be hard-asserted
+        newTargetTerms.push(term);
     }
 
-    assert(not fullCore or newNamedTerms.size() == 0);
-    terms = std::move(newTerms);
-    namedTerms = std::move(newNamedTerms);
+    return newTargetTerms;
 }
 
 } // namespace opensmt
diff --git a/src/unsatcores/UnsatCoreBuilder.h b/src/unsatcores/UnsatCoreBuilder.h
index 6e58e8f79..db8e4131a 100644
--- a/src/unsatcores/UnsatCoreBuilder.h
+++ b/src/unsatcores/UnsatCoreBuilder.h
@@ -13,59 +13,70 @@ namespace opensmt {
 
 class UnsatCore;
 
+class MainSolver;
+
 class Logic;
 class ResolutionProof;
 class PartitionManager;
-class TermNames;
-
-class MainSolver;
 
-class UnsatCoreBuilder {
+class UnsatCoreBuilderBase {
 public:
     using Proof = ResolutionProof;
 
-    UnsatCoreBuilder(SMTConfig const & conf, Logic & logic_, Proof const & proof_, PartitionManager const & pmanager,
-                     TermNames const & names)
-        : config{conf},
-          logic{logic_},
-          proof{proof_},
-          partitionManager{pmanager},
-          termNames{names} {}
+    UnsatCoreBuilderBase(MainSolver const &);
+
+protected:
+    MainSolver const & solver;
+    SMTConfig const & config;
+    Logic & logic;
+    Proof const & proof;
+    PartitionManager const & partitionManager;
+};
+
+class UnsatCoreBuilder : public UnsatCoreBuilderBase {
+public:
+    UnsatCoreBuilder(MainSolver const & solver_) : UnsatCoreBuilderBase(solver_) {}
 
     std::unique_ptr<UnsatCore> build();
 
 protected:
-    using SMTSolver = MainSolver;
+    class Minimize;
 
     void buildBody();
     std::unique_ptr<UnsatCore> buildReturn();
 
     void computeClauses();
-    void computeTerms();
-    void computeNamedTerms();
+    void mapClausesToTerms();
 
-    SMTConfig makeSmtSolverConfig() const;
-    std::unique_ptr<SMTSolver> newSmtSolver(SMTConfig &) const;
+    void partitionNamedTerms();
 
     void minimize();
 
-    void minimizeInit();
-    void minimizeAlg() { minimizeAlgNaive(); }
-    void minimizeFinish() {}
+    vec<CRef> clauses{};
+    vec<PTRef> allTerms{};
+    vec<PTRef> namedTerms{};
+    vec<PTRef> hiddenTerms{};
+};
 
-    void minimizeAlgNaive();
+class UnsatCoreBuilder::Minimize {
+public:
+    using InternalSMTSolver = MainSolver;
 
-    SMTConfig const & config;
-    Logic & logic;
-    Proof const & proof;
-    PartitionManager const & partitionManager;
-    TermNames const & termNames;
+    Minimize(UnsatCoreBuilder &, vec<PTRef> targetTerms, vec<PTRef> const & backgroundTerms_ = {});
+    ~Minimize();
 
-    vec<CRef> clauses{};
-    vec<PTRef> terms{};
-    vec<PTRef> namedTerms{};
+    vec<PTRef> perform() &&;
+
+protected:
+    SMTConfig makeSmtSolverConfig() const;
+    std::unique_ptr<InternalSMTSolver> newSmtSolver(SMTConfig &) const;
+
+    vec<PTRef> performNaive(InternalSMTSolver &);
+
+    UnsatCoreBuilder & builder;
 
-    std::vector<size_t> namedTermsIdxs{};
+    vec<PTRef> targetTerms;
+    vec<PTRef> const & backgroundTerms;
 };
 
 } // namespace opensmt
diff --git a/test/unit/test_UnsatCore.cc b/test/unit/test_UnsatCore.cc
index c8df9097e..cc61f36a6 100644
--- a/test/unit/test_UnsatCore.cc
+++ b/test/unit/test_UnsatCore.cc
@@ -51,6 +51,39 @@ class MinUnsatCoreTestBase {
     }
 };
 
+template <typename LogicT>
+class FullUnsatCoreTestBase {
+protected:
+    FullUnsatCoreTestBase(Logic_t type) : logic{type} {}
+
+    LogicT logic;
+    SMTConfig config;
+
+    MainSolver makeSolver() {
+        const char* msg = "ok";
+        config.setOption(SMTConfig::o_produce_unsat_cores, SMTOption(true), msg);
+        config.setOption(SMTConfig::o_print_cores_full, SMTOption(true), msg);
+        return {logic, config, "unsat_core"};
+    }
+};
+
+template <typename LogicT>
+class MinFullUnsatCoreTestBase {
+protected:
+    MinFullUnsatCoreTestBase(Logic_t type) : logic{type} {}
+
+    LogicT logic;
+    SMTConfig config;
+
+    MainSolver makeSolver() {
+        const char* msg = "ok";
+        config.setOption(SMTConfig::o_produce_unsat_cores, SMTOption(true), msg);
+        config.setOption(SMTConfig::o_print_cores_full, SMTOption(true), msg);
+        config.setOption(SMTConfig::o_minimal_unsat_cores, SMTOption(true), msg);
+        return {logic, config, "unsat_core"};
+    }
+};
+
 /// Pure propositional and uninterpreted functions
 template <template<typename> typename TestBaseT>
 class UFUnsatCoreTestTp : public ::testing::Test, public TestBaseT<Logic> {
@@ -85,12 +118,18 @@ class UFUnsatCoreTestTp : public ::testing::Test, public TestBaseT<Logic> {
 
 using UFUnsatCoreTest = UFUnsatCoreTestTp<UnsatCoreTestBase>;
 using MinUFUnsatCoreTest = UFUnsatCoreTestTp<MinUnsatCoreTestBase>;
+using FullUFUnsatCoreTest = UFUnsatCoreTestTp<FullUnsatCoreTestBase>;
+using MinFullUFUnsatCoreTest = UFUnsatCoreTestTp<MinFullUnsatCoreTestBase>;
 
 TEST_F(UFUnsatCoreTest, Bool_Simple) {
     MainSolver solver = makeSolver();
     solver.insertFormula(b1);
     solver.insertFormula(b2);
     solver.insertFormula(nb1);
+    auto & termNames = solver.getTermNames();
+    termNames.insert("a1", b1);
+    termNames.insert("a2", b2);
+    termNames.insert("a3", nb1);
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
@@ -112,7 +151,7 @@ TEST_F(MinUFUnsatCoreTest, Min_Bool_Simple) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
     EXPECT_TRUE(isInCore(b1, coreTerms));
     EXPECT_TRUE(isInCore(nb1, coreTerms));
@@ -129,7 +168,7 @@ TEST_F(MinUFUnsatCoreTest, Min_Bool_Simple_Unnamed1) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 1);
     EXPECT_FALSE(isInCore(b1, coreTerms));
     EXPECT_TRUE(isInCore(nb1, coreTerms));
@@ -146,7 +185,7 @@ TEST_F(MinUFUnsatCoreTest, Min_Bool_Simple_Unnamed2) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
     EXPECT_TRUE(isInCore(b1, coreTerms));
     EXPECT_TRUE(isInCore(nb1, coreTerms));
@@ -163,12 +202,91 @@ TEST_F(MinUFUnsatCoreTest, Min_Bool_Simple_Unnamed3) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 1);
     EXPECT_TRUE(isInCore(b1, coreTerms));
     EXPECT_FALSE(isInCore(nb1, coreTerms));
 }
 
+TEST_F(FullUFUnsatCoreTest, Full_Bool_Simple) {
+    MainSolver solver = makeSolver();
+    solver.insertFormula(b1);
+    solver.insertFormula(b2);
+    solver.insertFormula(nb1);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(b1, coreTerms));
+    EXPECT_TRUE(isInCore(nb1, coreTerms));
+}
+
+TEST_F(MinFullUFUnsatCoreTest, Min_Full_Bool_Simple) {
+    MainSolver solver = makeSolver();
+    solver.insertFormula(b1);
+    solver.insertFormula(b2);
+    solver.insertFormula(nb1);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(b1, coreTerms));
+    EXPECT_TRUE(isInCore(nb1, coreTerms));
+}
+
+TEST_F(MinFullUFUnsatCoreTest, Min_Full_Bool_Simple_Unnamed1) {
+    MainSolver solver = makeSolver();
+    solver.insertFormula(b1);
+    solver.insertFormula(b2);
+    solver.insertFormula(nb1);
+    auto & termNames = solver.getTermNames();
+    termNames.insert("a2", b2);
+    termNames.insert("a3", nb1);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(b1, coreTerms));
+    EXPECT_TRUE(isInCore(nb1, coreTerms));
+}
+
+TEST_F(MinFullUFUnsatCoreTest, Min_Full_Bool_Simple_Unnamed2) {
+    MainSolver solver = makeSolver();
+    solver.insertFormula(b1);
+    solver.insertFormula(b2);
+    solver.insertFormula(nb1);
+    auto & termNames = solver.getTermNames();
+    termNames.insert("a1", b1);
+    termNames.insert("a3", nb1);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(b1, coreTerms));
+    EXPECT_TRUE(isInCore(nb1, coreTerms));
+}
+
+TEST_F(MinFullUFUnsatCoreTest, Min_Full_Bool_Simple_Unnamed3) {
+    MainSolver solver = makeSolver();
+    solver.insertFormula(b1);
+    solver.insertFormula(b2);
+    solver.insertFormula(nb1);
+    auto & termNames = solver.getTermNames();
+    termNames.insert("a1", b1);
+    termNames.insert("a2", b2);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(b1, coreTerms));
+    EXPECT_TRUE(isInCore(nb1, coreTerms));
+}
+
 TEST_F(UFUnsatCoreTest, Bool_ReuseProofChain) {
     // We add three assertions
     // a1 := (b1 or b2) and (b1 or ~b2)
@@ -185,6 +303,10 @@ TEST_F(UFUnsatCoreTest, Bool_ReuseProofChain) {
     solver.insertFormula(a1);
     solver.insertFormula(a2);
     solver.insertFormula(b4);
+    auto & termNames = solver.getTermNames();
+    termNames.insert("a1", a1);
+    termNames.insert("a2", a2);
+    termNames.insert("a3", b4);
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
@@ -218,7 +340,33 @@ TEST_F(MinUFUnsatCoreTest, Min_Bool_ReuseProofChain) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_TRUE(isInCore(a2, coreTerms));
+    EXPECT_FALSE(isInCore(b4, coreTerms));
+}
+
+TEST_F(FullUFUnsatCoreTest, Full_Bool_ReuseProofChain) {
+    // We add three assertions
+    // a1 := (b1 or b2) and (b1 or ~b2)
+    // a2 := (~b1 or b3) and (~b1 or ~b3)
+    // a3 := b4
+    // The first two assertions form the unsat core.
+    MainSolver solver = makeSolver();
+    PTRef c1 = logic.mkOr(b1, b2);
+    PTRef c2 = logic.mkOr(b1, nb2);
+    PTRef c3 = logic.mkOr(nb1, b3);
+    PTRef c4 = logic.mkOr(nb1, nb3);
+    PTRef a1 = logic.mkAnd(c1,c2);
+    PTRef a2 = logic.mkAnd(c3,c4);
+    solver.insertFormula(a1);
+    solver.insertFormula(a2);
+    solver.insertFormula(b4);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
     EXPECT_TRUE(isInCore(a1, coreTerms));
     EXPECT_TRUE(isInCore(a2, coreTerms));
@@ -236,6 +384,10 @@ TEST_F(UFUnsatCoreTest, UF_Simple) {
     solver.insertFormula(a1);
     solver.insertFormula(a2);
     solver.insertFormula(a3);
+    auto & termNames = solver.getTermNames();
+    termNames.insert("a1", a1);
+    termNames.insert("a2", a2);
+    termNames.insert("a3", a3);
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
@@ -264,7 +416,7 @@ TEST_F(MinUFUnsatCoreTest, Min_UF_Simple) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
     EXPECT_TRUE(isInCore(a1, coreTerms));
     EXPECT_FALSE(isInCore(a2, coreTerms));
@@ -288,7 +440,7 @@ TEST_F(MinUFUnsatCoreTest, Min_UF_Simple_Unnamed1) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 1);
     EXPECT_FALSE(isInCore(a1, coreTerms));
     EXPECT_FALSE(isInCore(a2, coreTerms));
@@ -312,7 +464,7 @@ TEST_F(MinUFUnsatCoreTest, Min_UF_Simple_Unnamed2) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
     EXPECT_TRUE(isInCore(a1, coreTerms));
     EXPECT_FALSE(isInCore(a2, coreTerms));
@@ -336,13 +488,34 @@ TEST_F(MinUFUnsatCoreTest, Min_UF_Simple_Unnamed3) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 1);
     EXPECT_TRUE(isInCore(a1, coreTerms));
     EXPECT_FALSE(isInCore(a2, coreTerms));
     EXPECT_FALSE(isInCore(a3, coreTerms));
 }
 
+TEST_F(FullUFUnsatCoreTest, Full_UF_Simple) {
+    // a1 := x = y
+    // a2 := g(x,y) = g(y,x)
+    // a3 := f(x) != f(y)
+    MainSolver solver = makeSolver();
+    PTRef a1 = logic.mkEq(x,y);
+    PTRef a2 = logic.mkEq(logic.mkUninterpFun(g,{x,y}), logic.mkUninterpFun(g,{y,x}));
+    PTRef a3 = logic.mkNot(logic.mkEq(logic.mkUninterpFun(f,{x}), logic.mkUninterpFun(f,{y})));
+    solver.insertFormula(a1);
+    solver.insertFormula(a2);
+    solver.insertFormula(a3);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_FALSE(isInCore(a2, coreTerms));
+    EXPECT_TRUE(isInCore(a3, coreTerms));
+}
+
 TEST_F(UFUnsatCoreTest, Bool_Simple_Overlap) {
     MainSolver solver = makeSolver();
     PTRef a1 = b1;
@@ -351,6 +524,10 @@ TEST_F(UFUnsatCoreTest, Bool_Simple_Overlap) {
     solver.insertFormula(a1);
     solver.insertFormula(a2);
     solver.insertFormula(a3);
+    auto & termNames = solver.getTermNames();
+    termNames.insert("a1", a1);
+    termNames.insert("a2", a2);
+    termNames.insert("a3", a3);
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
@@ -376,13 +553,31 @@ TEST_F(MinUFUnsatCoreTest, Min_Bool_Simple_Overlap) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
     EXPECT_FALSE(isInCore(a1, coreTerms));
     EXPECT_TRUE(isInCore(a2, coreTerms));
     EXPECT_TRUE(isInCore(a3, coreTerms));
 }
 
+TEST_F(FullUFUnsatCoreTest, Full_Bool_Simple_Overlap) {
+    MainSolver solver = makeSolver();
+    PTRef a1 = b1;
+    PTRef a2 = logic.mkAnd(b1, b2);
+    PTRef a3 = logic.mkOr(logic.mkNot(b1), logic.mkNot(b2));
+    solver.insertFormula(a1);
+    solver.insertFormula(a2);
+    solver.insertFormula(a3);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getTerms();
+    ASSERT_EQ(coreTerms.size(), 3);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_TRUE(isInCore(a2, coreTerms));
+    EXPECT_TRUE(isInCore(a3, coreTerms));
+}
+
 /// Pure arrays
 template <template<typename> typename TestBaseT>
 class AXUnsatCoreTestTp : public ::testing::Test, public TestBaseT<Logic> {
@@ -409,6 +604,7 @@ class AXUnsatCoreTestTp : public ::testing::Test, public TestBaseT<Logic> {
 
 using AXUnsatCoreTest = AXUnsatCoreTestTp<UnsatCoreTestBase>;
 using MinAXUnsatCoreTest = AXUnsatCoreTestTp<MinUnsatCoreTestBase>;
+using FullAXUnsatCoreTest = AXUnsatCoreTestTp<FullUnsatCoreTestBase>;
 
 TEST_F(AXUnsatCoreTest, AX_Simple) {
     // a1 := i != j
@@ -421,6 +617,10 @@ TEST_F(AXUnsatCoreTest, AX_Simple) {
     solver.insertFormula(a1);
     solver.insertFormula(a2);
     solver.insertFormula(a3);
+    auto & termNames = solver.getTermNames();
+    termNames.insert("a1", a1);
+    termNames.insert("a2", a2);
+    termNames.insert("a3", a3);
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
@@ -449,7 +649,28 @@ TEST_F(AXUnsatCoreTest, Min_AX_Simple) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_TRUE(isInCore(a2, coreTerms));
+    EXPECT_FALSE(isInCore(a3, coreTerms));
+}
+
+TEST_F(FullAXUnsatCoreTest, Full_AX_Simple) {
+    // a1 := i != j
+    // a2 := a[j] != a<i -> e>[j]
+    // a3 := a[k] = e
+    MainSolver solver = makeSolver();
+    PTRef a1 = logic.mkNot(logic.mkEq(i,j));
+    PTRef a2 = logic.mkNot(logic.mkEq(logic.mkSelect({a,j}), logic.mkSelect({logic.mkStore({a,i,e}),j})));
+    PTRef a3 = logic.mkEq(logic.mkSelect({a,k}), e);
+    solver.insertFormula(a1);
+    solver.insertFormula(a2);
+    solver.insertFormula(a3);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
     EXPECT_TRUE(isInCore(a1, coreTerms));
     EXPECT_TRUE(isInCore(a2, coreTerms));
@@ -486,6 +707,7 @@ class LIAUnsatCoreTestTp : public ::testing::Test, public TestBaseT<ArithLogic>
 
 using LIAUnsatCoreTest = LIAUnsatCoreTestTp<UnsatCoreTestBase>;
 using MinLIAUnsatCoreTest = LIAUnsatCoreTestTp<MinUnsatCoreTestBase>;
+using FullLIAUnsatCoreTest = LIAUnsatCoreTestTp<FullUnsatCoreTestBase>;
 
 TEST_F(LIAUnsatCoreTest, LIA_Simple) {
     // a1 := x >= y
@@ -501,6 +723,11 @@ TEST_F(LIAUnsatCoreTest, LIA_Simple) {
     solver.insertFormula(a2);
     solver.insertFormula(a3);
     solver.insertFormula(a4);
+    auto & termNames = solver.getTermNames();
+    termNames.insert("a1", a1);
+    termNames.insert("a2", a2);
+    termNames.insert("a3", a3);
+    termNames.insert("a4", a4);
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
@@ -534,7 +761,32 @@ TEST_F(LIAUnsatCoreTest, Min_LIA_Simple) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
+    ASSERT_EQ(coreTerms.size(), 3);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_TRUE(isInCore(a2, coreTerms));
+    EXPECT_FALSE(isInCore(a3, coreTerms));
+    EXPECT_TRUE(isInCore(a4, coreTerms));
+}
+
+TEST_F(FullLIAUnsatCoreTest, Full_LIA_Simple) {
+    // a1 := x >= y
+    // a2 := y >= z
+    // a3 := x + y + z < 0
+    // a4 := x < z
+    MainSolver solver = makeSolver();
+    PTRef a1 = logic.mkGeq(x,y);
+    PTRef a2 = logic.mkGeq(y,z);
+    PTRef a3 = logic.mkLt(logic.mkPlus(vec<PTRef>{x,y,z}), logic.getTerm_IntZero());
+    PTRef a4 = logic.mkLt(x,z);
+    solver.insertFormula(a1);
+    solver.insertFormula(a2);
+    solver.insertFormula(a3);
+    solver.insertFormula(a4);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 3);
     EXPECT_TRUE(isInCore(a1, coreTerms));
     EXPECT_TRUE(isInCore(a2, coreTerms));
@@ -576,6 +828,7 @@ class ALIAUnsatCoreTestTp : public ::testing::Test, public TestBaseT<ArithLogic>
 
 using ALIAUnsatCoreTest = ALIAUnsatCoreTestTp<UnsatCoreTestBase>;
 using MinALIAUnsatCoreTest = ALIAUnsatCoreTestTp<MinUnsatCoreTestBase>;
+using FullALIAUnsatCoreTest = ALIAUnsatCoreTestTp<FullUnsatCoreTestBase>;
 
 TEST_F(ALIAUnsatCoreTest, ALIA_Simple) {
     // a1 := select(arr1, x) != select(arr1,y)
@@ -588,6 +841,10 @@ TEST_F(ALIAUnsatCoreTest, ALIA_Simple) {
     solver.insertFormula(a1);
     solver.insertFormula(a2);
     solver.insertFormula(a3);
+    auto & termNames = solver.getTermNames();
+    termNames.insert("a1", a1);
+    termNames.insert("a2", a2);
+    termNames.insert("a3", a3);
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
@@ -616,7 +873,28 @@ TEST_F(ALIAUnsatCoreTest, Min_ALIA_Simple) {
     auto res = solver.check();
     ASSERT_EQ(res, s_False);
     auto core = solver.getUnsatCore();
-    auto & coreTerms = core->getNamedTerms();
+    auto & coreTerms = core->getTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_FALSE(isInCore(a2, coreTerms));
+    EXPECT_TRUE(isInCore(a3, coreTerms));
+}
+
+TEST_F(FullALIAUnsatCoreTest, Full_ALIA_Simple) {
+    // a1 := select(arr1, x) != select(arr1,y)
+    // a2 := select(arr1, x) == 0
+    // a3 := x == y
+    MainSolver solver = makeSolver();
+    PTRef a1 = logic.mkNot(logic.mkEq(logic.mkSelect({arr1, x}), logic.mkSelect({arr1,y})));
+    PTRef a2 = logic.mkEq(logic.mkSelect({arr1,x}), logic.getTerm_IntZero());
+    PTRef a3 = logic.mkEq(x,y);
+    solver.insertFormula(a1);
+    solver.insertFormula(a2);
+    solver.insertFormula(a3);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
     EXPECT_TRUE(isInCore(a1, coreTerms));
     EXPECT_FALSE(isInCore(a2, coreTerms));