diff --git a/src/api/MainSolver.cc b/src/api/MainSolver.cc
index 136a4247b..0a86ec3d3 100644
--- a/src/api/MainSolver.cc
+++ b/src/api/MainSolver.cc
@@ -231,7 +231,8 @@ 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"); }
 
-    UnsatCoreBuilder unsatCoreBuilder{config, smt_solver->getResolutionProof(), pmanager, termNames};
+    auto & proof = smt_solver->getResolutionProof();
+    UnsatCoreBuilder unsatCoreBuilder{config, logic, proof, pmanager, termNames};
 
     return unsatCoreBuilder.build();
 }
diff --git a/src/options/SMTConfig.cc b/src/options/SMTConfig.cc
index bb520819e..fe0488f98 100644
--- a/src/options/SMTConfig.cc
+++ b/src/options/SMTConfig.cc
@@ -447,6 +447,7 @@ namespace opensmt {
 
   const char* SMTConfig::o_produce_models = ":produce-models";
   const char* SMTConfig::o_produce_unsat_cores = ":produce-unsat-cores";
+  const char* SMTConfig::o_minimal_unsat_cores = ":minimal-unsat-cores";
   const char* SMTConfig::o_verbosity      = ":verbosity";
   const char* SMTConfig::o_incremental    = ":incremental";
   const char* SMTConfig::o_produce_stats  = ":produce-stats";
diff --git a/src/options/SMTConfig.h b/src/options/SMTConfig.h
index 4c2df1f9e..781fd8085 100644
--- a/src/options/SMTConfig.h
+++ b/src/options/SMTConfig.h
@@ -306,6 +306,8 @@ namespace opensmt {
     static const char* o_sat_split_randomize_lookahead_buf;
     static const char* o_produce_models;
     static const char* o_produce_unsat_cores;
+    // Produce the unsat cores as locally minimal (i.e. subset-minimal)
+    static const char* o_minimal_unsat_cores;
     static const char* o_sat_remove_symmetries;
     static const char* o_dryrun;
     static const char* o_do_substitutions;
@@ -515,6 +517,9 @@ namespace opensmt {
     bool produce_unsat_cores() const {
         return optionTable.has(o_produce_unsat_cores) && optionTable[o_produce_unsat_cores]->getValue().numval > 0;
     }
+    bool minimal_unsat_cores() const {
+        return optionTable.has(o_minimal_unsat_cores) && optionTable[o_minimal_unsat_cores]->getValue().numval > 0;
+    }
     int          produceStats() const
       { return optionTable.has(o_produce_stats) ?
           optionTable[o_produce_stats]->getValue().numval == 1: false; }
diff --git a/src/parsers/smt2new/smt2newlexer.ll b/src/parsers/smt2new/smt2newlexer.ll
index b55b330a4..8d48ab8c7 100644
--- a/src/parsers/smt2new/smt2newlexer.ll
+++ b/src/parsers/smt2new/smt2newlexer.ll
@@ -117,6 +117,7 @@ using namespace opensmt::tokens;
 ":interactive-mode"          { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_INTERACTIVEMODE;         }
 ":produce-proofs"            { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRODUCEPROOFS;           }
 ":produce-unsat-cores"       { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRODUCEUNSATCORES;       }
+":minimal-unsat-cores"       { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_MINIMALUNSATCORES;       }
 ":produce-models"            { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRODUCEMODELS;           }
 ":produce-assignments"       { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRODUCEASSIGNMENTS;      }
 ":regular-output-channel"    { yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_REGULAROUTPUTCHANNEL;    }
diff --git a/src/parsers/smt2new/smt2newparser.yy b/src/parsers/smt2new/smt2newparser.yy
index 17bb1c862..09535b280 100644
--- a/src/parsers/smt2new/smt2newparser.yy
+++ b/src/parsers/smt2new/smt2newparser.yy
@@ -84,13 +84,13 @@ void osmt_yyerror( YYLTYPE* locp, Smt2newContext* context, const char * s )
 %token TK_AS TK_DECIMAL TK_EXISTS TK_FORALL TK_LET TK_NUMERAL TK_PAR TK_STRING
 %token TK_ASSERT TK_CHECKSAT TK_DECLARESORT TK_DECLAREFUN TK_DECLARECONST TK_DEFINESORT TK_DEFINEFUN TK_EXIT TK_GETASSERTIONS TK_GETASSIGNMENT TK_GETINFO TK_GETOPTION TK_GETPROOF TK_GETUNSATCORE TK_GETVALUE TK_GETMODEL TK_POP TK_PUSH TK_SETLOGIC TK_SETINFO TK_SETOPTION TK_THEORY TK_GETITPS TK_WRSTATE TK_RDSTATE TK_SIMPLIFY TK_WRFUNS TK_ECHO
 %token TK_NUM TK_SYM TK_QSYM TK_KEY TK_STR TK_DEC TK_HEX TK_BIN
-%token KW_SORTS KW_FUNS KW_SORTSDESCRIPTION KW_FUNSDESCRIPTION KW_DEFINITION KW_NOTES KW_THEORIES KW_EXTENSIONS KW_VALUES KW_PRINTSUCCESS KW_EXPANDDEFINITIONS KW_INTERACTIVEMODE KW_PRODUCEPROOFS KW_PRODUCEUNSATCORES KW_PRODUCEMODELS KW_PRODUCEASSIGNMENTS KW_REGULAROUTPUTCHANNEL KW_DIAGNOSTICOUTPUTCHANNEL KW_RANDOMSEED KW_VERBOSITY KW_ERRORBEHAVIOR KW_NAME KW_NAMED KW_AUTHORS KW_VERSION KW_STATUS KW_REASONUNKNOWN KW_ALLSTATISTICS
+%token KW_SORTS KW_FUNS KW_SORTSDESCRIPTION KW_FUNSDESCRIPTION KW_DEFINITION KW_NOTES KW_THEORIES KW_EXTENSIONS KW_VALUES KW_PRINTSUCCESS KW_EXPANDDEFINITIONS KW_INTERACTIVEMODE KW_PRODUCEPROOFS KW_PRODUCEUNSATCORES KW_MINIMALUNSATCORES KW_PRODUCEMODELS KW_PRODUCEASSIGNMENTS KW_REGULAROUTPUTCHANNEL KW_DIAGNOSTICOUTPUTCHANNEL KW_RANDOMSEED KW_VERBOSITY KW_ERRORBEHAVIOR KW_NAME KW_NAMED KW_AUTHORS KW_VERSION KW_STATUS KW_REASONUNKNOWN KW_ALLSTATISTICS
 
 %type <tok> TK_AS TK_DECIMAL TK_EXISTS TK_FORALL TK_LET TK_NUMERAL TK_PAR TK_STRING
 %type <tok> TK_ASSERT TK_CHECKSAT TK_DECLARESORT TK_DECLAREFUN TK_DECLARECONST TK_DEFINESORT TK_DEFINEFUN TK_EXIT TK_GETASSERTIONS TK_GETASSIGNMENT TK_GETINFO TK_GETOPTION TK_GETPROOF TK_GETUNSATCORE TK_GETVALUE TK_GETMODEL TK_POP TK_PUSH TK_SETLOGIC TK_SETINFO TK_SETOPTION TK_THEORY TK_GETITPS TK_WRSTATE TK_RDSTATE TK_SIMPLIFY TK_WRFUNS TK_ECHO
 
 %type <str> TK_NUM TK_SYM TK_QSYM TK_KEY TK_STR TK_DEC TK_HEX TK_BIN
-%type <str> KW_SORTS KW_FUNS KW_SORTSDESCRIPTION KW_FUNSDESCRIPTION KW_DEFINITION KW_NOTES KW_THEORIES KW_EXTENSIONS KW_VALUES KW_PRINTSUCCESS KW_EXPANDDEFINITIONS KW_INTERACTIVEMODE KW_PRODUCEPROOFS KW_PRODUCEUNSATCORES KW_PRODUCEMODELS KW_PRODUCEASSIGNMENTS KW_REGULAROUTPUTCHANNEL KW_DIAGNOSTICOUTPUTCHANNEL KW_RANDOMSEED KW_VERBOSITY KW_ERRORBEHAVIOR KW_NAME KW_NAMED KW_AUTHORS KW_VERSION KW_STATUS KW_REASONUNKNOWN KW_ALLSTATISTICS predef_key
+%type <str> KW_SORTS KW_FUNS KW_SORTSDESCRIPTION KW_FUNSDESCRIPTION KW_DEFINITION KW_NOTES KW_THEORIES KW_EXTENSIONS KW_VALUES KW_PRINTSUCCESS KW_EXPANDDEFINITIONS KW_INTERACTIVEMODE KW_PRODUCEPROOFS KW_PRODUCEUNSATCORES KW_MINIMALUNSATCORES KW_PRODUCEMODELS KW_PRODUCEASSIGNMENTS KW_REGULAROUTPUTCHANNEL KW_DIAGNOSTICOUTPUTCHANNEL KW_RANDOMSEED KW_VERBOSITY KW_ERRORBEHAVIOR KW_NAME KW_NAMED KW_AUTHORS KW_VERSION KW_STATUS KW_REASONUNKNOWN KW_ALLSTATISTICS predef_key
 %type <snode> symbol identifier sort command attribute attribute_value s_expr spec_const qual_identifier var_binding sorted_var term const_val
 %type <snode_list> sort_list command_list s_expr_list numeral_list term_list var_binding_list attribute_list sorted_var_list symbol_list
 %type <snode> b_value option info_flag
@@ -539,6 +539,12 @@ option: KW_PRINTSUCCESS b_value
             $$->children = new std::vector<ASTNode*>();
             $$->children->push_back($2);
         }
+    | KW_MINIMALUNSATCORES b_value
+        {
+            $$ = new ASTNode(OPTION_T, $1);
+            $$->children = new std::vector<ASTNode*>();
+            $$->children->push_back($2);
+        }
     | KW_PRODUCEMODELS b_value
         {
             $$ = new ASTNode(OPTION_T, $1);
@@ -611,6 +617,8 @@ predef_key: KW_SORTS
         { $$ = $1; }
     | KW_PRODUCEUNSATCORES
         { $$ = $1; }
+    | KW_MINIMALUNSATCORES
+        { $$ = $1; }
     | KW_PRODUCEMODELS
         { $$ = $1; }
     | KW_PRODUCEASSIGNMENTS
diff --git a/src/unsatcores/UnsatCoreBuilder.cc b/src/unsatcores/UnsatCoreBuilder.cc
index 1629c4619..4303bbc3e 100644
--- a/src/unsatcores/UnsatCoreBuilder.cc
+++ b/src/unsatcores/UnsatCoreBuilder.cc
@@ -1,10 +1,12 @@
 
 #include "UnsatCoreBuilder.h"
 
+#include <api/MainSolver.h>
 #include <api/PartitionManager.h>
 #include <common/PartitionInfo.h>
 #include <common/TermNames.h>
 #include <interpolation/InterpolationUtils.h>
+#include <logics/Logic.h>
 #include <smtsolvers/ResolutionProof.h>
 
 #include <unordered_set>
@@ -14,11 +16,55 @@ namespace opensmt {
 
 using Partitions = ipartitions_t;
 
+std::unique_ptr<SMTConfig> UnsatCoreBuilder::newSmtSolverConfig() const {
+    assert(config.minimal_unsat_cores());
+
+    SMTConfig newConfig;
+    assert(newConfig.isIncremental());
+    assert(newConfig.verbosity() == 0);
+    assert(not newConfig.printSuccess());
+    assert(not newConfig.produceStats());
+    assert(not newConfig.produce_unsat_cores());
+    assert(not newConfig.produce_proof());
+    assert(not newConfig.produce_inter());
+
+    char const * msg = "ok";
+    newConfig.setOption(SMTConfig::o_produce_models, SMTOption(false), msg);
+    assert(not newConfig.produce_models());
+
+    return std::make_unique<SMTConfig>(std::move(newConfig));
+}
+
+std::unique_ptr<UnsatCoreBuilder::SMTSolver> UnsatCoreBuilder::newSmtSolver() const {
+    assert(config.minimal_unsat_cores());
+
+    return std::make_unique<SMTSolver>(logic, *smtSolverConfigPtr, "unsat core solver");
+}
+
+void UnsatCoreBuilder::setSmtSolverConfig() {
+    assert(not smtSolverConfigPtr);
+    smtSolverConfigPtr = newSmtSolverConfig();
+}
+
+void UnsatCoreBuilder::setSmtSolver() {
+    assert(not smtSolverPtr);
+    smtSolverPtr = newSmtSolver();
+}
+
 std::unique_ptr<UnsatCore> UnsatCoreBuilder::build() {
+    buildBody();
+    return buildReturn();
+}
+
+void UnsatCoreBuilder::buildBody() {
     computeClauses();
     computeTerms();
     computeNamedTerms();
 
+    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)}};
 }
@@ -65,12 +111,84 @@ void UnsatCoreBuilder::computeTerms() {
 void UnsatCoreBuilder::computeNamedTerms() {
     assert(terms.size() > 0);
     namedTerms.clear();
+    namedTermsIdxs.clear();
 
     if (termNames.empty()) return;
 
-    for (PTRef term : terms) {
-        if (termNames.contains(term)) { namedTerms.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);
     }
 }
 
+void UnsatCoreBuilder::minimize() {
+    minimizeInit();
+    minimizeAlg();
+    minimizeFinish();
+}
+
+void UnsatCoreBuilder::minimizeInit() {
+    assert(terms.size() >= namedTerms.size());
+    assert(size_t(namedTerms.size()) == namedTermsIdxs.size());
+
+    setSmtSolverConfig();
+    setSmtSolver();
+}
+
+void UnsatCoreBuilder::minimizeAlgNaive() {
+    if (namedTerms.size() == 0) return;
+
+    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);
+    };
+    decltype(terms) newTerms;
+    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;
+        }
+        PTRef term = terms[idx];
+        smtSolverPtr->insertFormula(term);
+        newTerms.push(term);
+    }
+
+    decltype(terms) newNamedTerms;
+    size_t const namedTermsSize = namedTerms.size();
+    for (size_t namedIdx = 0; namedIdx < namedTermsSize; ++namedIdx) {
+        smtSolverPtr->push();
+
+        // try to ignore namedTerms[namedIdx]
+
+        for (size_t keptNamedIdx = namedIdx + 1; keptNamedIdx < namedTermsSize; ++keptNamedIdx) {
+            PTRef term = namedTerms[keptNamedIdx];
+            smtSolverPtr->insertFormula(term);
+        }
+
+        sstat const res = smtSolverPtr->check();
+        assert(res == s_True || res == s_False);
+        bool const isRedundant = (res == s_False);
+
+        smtSolverPtr->pop();
+
+        if (isRedundant) continue;
+
+        // namedTerms[namedIdx] is not redundant - include it
+
+        PTRef term = namedTerms[namedIdx];
+        smtSolverPtr->insertFormula(term);
+        newTerms.push(term);
+        newNamedTerms.push(term);
+    }
+
+    terms = std::move(newTerms);
+    namedTerms = std::move(newNamedTerms);
+}
+
 } // namespace opensmt
diff --git a/src/unsatcores/UnsatCoreBuilder.h b/src/unsatcores/UnsatCoreBuilder.h
index d3b1316ea..6240a603c 100644
--- a/src/unsatcores/UnsatCoreBuilder.h
+++ b/src/unsatcores/UnsatCoreBuilder.h
@@ -7,22 +7,27 @@
 #include <options/SMTConfig.h>
 
 #include <memory>
+#include <vector>
 
 namespace opensmt {
 
 class UnsatCore;
 
+class Logic;
 class ResolutionProof;
 class PartitionManager;
 class TermNames;
 
+class MainSolver;
+
 class UnsatCoreBuilder {
 public:
     using Proof = ResolutionProof;
 
-    UnsatCoreBuilder(SMTConfig const & conf, Proof const & proof_, PartitionManager const & pmanager,
+    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} {}
@@ -30,19 +35,42 @@ class UnsatCoreBuilder {
     std::unique_ptr<UnsatCore> build();
 
 protected:
+    using SMTSolver = MainSolver;
+
+    std::unique_ptr<SMTConfig> newSmtSolverConfig() const;
+    std::unique_ptr<SMTSolver> newSmtSolver() const;
+    void setSmtSolverConfig();
+    void setSmtSolver();
+
+    void buildBody();
+    std::unique_ptr<UnsatCore> buildReturn();
+
     void computeClauses();
     void computeTerms();
     void computeNamedTerms();
 
+    void minimize();
+
+    void minimizeInit();
+    void minimizeAlg() { minimizeAlgNaive(); }
+    void minimizeFinish() {}
+
+    void minimizeAlgNaive();
+
     SMTConfig const & config;
+    Logic & logic;
     Proof const & proof;
     PartitionManager const & partitionManager;
     TermNames const & termNames;
 
-private:
-    vec<CRef> clauses;
-    vec<PTRef> terms;
-    vec<PTRef> namedTerms;
+    vec<CRef> clauses{};
+    vec<PTRef> terms{};
+    vec<PTRef> namedTerms{};
+
+    std::vector<size_t> namedTermsIdxs{};
+
+    std::unique_ptr<SMTConfig> smtSolverConfigPtr{};
+    std::unique_ptr<SMTSolver> smtSolverPtr{};
 };
 
 } // namespace opensmt
diff --git a/test/regression/base/generic/overlap_min_unsat_core.smt2 b/test/regression/base/generic/overlap_min_unsat_core.smt2
new file mode 100644
index 000000000..38eefc0c5
--- /dev/null
+++ b/test/regression/base/generic/overlap_min_unsat_core.smt2
@@ -0,0 +1,11 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+(set-logic QF_UF)
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(assert (! b1 :named a1))
+(assert (! (and b1 b2) :named a2))
+(assert (! (or (not b1) (not b2)) :named a3))
+(check-sat)
+(get-unsat-core)
+(exit)
diff --git a/test/regression/base/generic/overlap_min_unsat_core.smt2.expected.err b/test/regression/base/generic/overlap_min_unsat_core.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/generic/overlap_min_unsat_core.smt2.expected.out b/test/regression/base/generic/overlap_min_unsat_core.smt2.expected.out
new file mode 100644
index 000000000..279e5a3a8
--- /dev/null
+++ b/test/regression/base/generic/overlap_min_unsat_core.smt2.expected.out
@@ -0,0 +1,2 @@
+unsat
+( a2 a3 )
diff --git a/test/regression/base/generic/overlap_unsat_core.smt2 b/test/regression/base/generic/overlap_unsat_core.smt2
new file mode 100644
index 000000000..694e812c3
--- /dev/null
+++ b/test/regression/base/generic/overlap_unsat_core.smt2
@@ -0,0 +1,10 @@
+(set-option :produce-unsat-cores true)
+(set-logic QF_UF)
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(assert (! b1 :named a1))
+(assert (! (and b1 b2) :named a2))
+(assert (! (or (not b1) (not b2)) :named a3))
+(check-sat)
+(get-unsat-core)
+(exit)
diff --git a/test/regression/base/generic/overlap_unsat_core.smt2.expected.err b/test/regression/base/generic/overlap_unsat_core.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/generic/overlap_unsat_core.smt2.expected.out b/test/regression/base/generic/overlap_unsat_core.smt2.expected.out
new file mode 100644
index 000000000..f321ff45e
--- /dev/null
+++ b/test/regression/base/generic/overlap_unsat_core.smt2.expected.out
@@ -0,0 +1,2 @@
+unsat
+( a1 a2 a3 )
diff --git a/test/regression/base/generic/redundant_min_unsat_core.smt2 b/test/regression/base/generic/redundant_min_unsat_core.smt2
new file mode 100644
index 000000000..28e650eed
--- /dev/null
+++ b/test/regression/base/generic/redundant_min_unsat_core.smt2
@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert (! b1 :named a1))
+(assert (! b2 :named a2))
+(assert (! (not b1) :named a3))
+(assert (! (and b1 b2) :named x1))
+(assert (! (or b1 b2) :named x2))
+(assert (! (xor b1 b2) :named x3))
+
+(check-sat)
+(get-unsat-core)
diff --git a/test/regression/base/generic/redundant_min_unsat_core.smt2.expected.err b/test/regression/base/generic/redundant_min_unsat_core.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/generic/redundant_min_unsat_core.smt2.expected.out b/test/regression/base/generic/redundant_min_unsat_core.smt2.expected.out
new file mode 100644
index 000000000..05da5c75d
--- /dev/null
+++ b/test/regression/base/generic/redundant_min_unsat_core.smt2.expected.out
@@ -0,0 +1,2 @@
+unsat
+( a1 a3 )
diff --git a/test/regression/base/generic/redundant_min_unsat_core2.smt2 b/test/regression/base/generic/redundant_min_unsat_core2.smt2
new file mode 100644
index 000000000..20942623b
--- /dev/null
+++ b/test/regression/base/generic/redundant_min_unsat_core2.smt2
@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert (! (and b1 b2) :named x1))
+(assert (! (or b1 b2) :named x2))
+(assert (! (xor b1 b2) :named x3))
+(assert (! b1 :named a1))
+(assert (! b2 :named a2))
+(assert (! (not b1) :named a3))
+
+(check-sat)
+(get-unsat-core)
diff --git a/test/regression/base/generic/redundant_min_unsat_core2.smt2.expected.err b/test/regression/base/generic/redundant_min_unsat_core2.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/generic/redundant_min_unsat_core2.smt2.expected.out b/test/regression/base/generic/redundant_min_unsat_core2.smt2.expected.out
new file mode 100644
index 000000000..ce29f3376
--- /dev/null
+++ b/test/regression/base/generic/redundant_min_unsat_core2.smt2.expected.out
@@ -0,0 +1,2 @@
+unsat
+( x1 x3 )
diff --git a/test/regression/base/generic/redundant_min_unsat_core3.smt2 b/test/regression/base/generic/redundant_min_unsat_core3.smt2
new file mode 100644
index 000000000..abab88da3
--- /dev/null
+++ b/test/regression/base/generic/redundant_min_unsat_core3.smt2
@@ -0,0 +1,17 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert (and b1 b2))
+(assert (or b1 b2))
+(assert (xor b1 b2))
+(assert (! b1 :named a1))
+(assert (! b2 :named a2))
+(assert (! (not b1) :named a3))
+
+(check-sat)
+(get-unsat-core)
diff --git a/test/regression/base/generic/redundant_min_unsat_core3.smt2.expected.err b/test/regression/base/generic/redundant_min_unsat_core3.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/generic/redundant_min_unsat_core3.smt2.expected.out b/test/regression/base/generic/redundant_min_unsat_core3.smt2.expected.out
new file mode 100644
index 000000000..15f932549
--- /dev/null
+++ b/test/regression/base/generic/redundant_min_unsat_core3.smt2.expected.out
@@ -0,0 +1,2 @@
+unsat
+( )
diff --git a/test/regression/base/generic/trivial_min_unsat_core.smt2 b/test/regression/base/generic/trivial_min_unsat_core.smt2
new file mode 100644
index 000000000..ea59747a5
--- /dev/null
+++ b/test/regression/base/generic/trivial_min_unsat_core.smt2
@@ -0,0 +1,11 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+(set-logic QF_UF)
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(assert (! b1 :named a1))
+(assert (! b2 :named a2))
+(assert (! (not b1) :named a3))
+(check-sat)
+(get-unsat-core)
+(exit)
diff --git a/test/regression/base/generic/trivial_min_unsat_core.smt2.expected.err b/test/regression/base/generic/trivial_min_unsat_core.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/generic/trivial_min_unsat_core.smt2.expected.out b/test/regression/base/generic/trivial_min_unsat_core.smt2.expected.out
new file mode 100644
index 000000000..05da5c75d
--- /dev/null
+++ b/test/regression/base/generic/trivial_min_unsat_core.smt2.expected.out
@@ -0,0 +1,2 @@
+unsat
+( a1 a3 )
diff --git a/test/regression/base/generic/trivial_min_unsat_core2.smt2 b/test/regression/base/generic/trivial_min_unsat_core2.smt2
new file mode 100644
index 000000000..fa45451de
--- /dev/null
+++ b/test/regression/base/generic/trivial_min_unsat_core2.smt2
@@ -0,0 +1,11 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+(set-logic QF_UF)
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(assert b1)
+(assert (! b2 :named a2))
+(assert (! (not b1) :named a3))
+(check-sat)
+(get-unsat-core)
+(exit)
diff --git a/test/regression/base/generic/trivial_min_unsat_core2.smt2.expected.err b/test/regression/base/generic/trivial_min_unsat_core2.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/generic/trivial_min_unsat_core2.smt2.expected.out b/test/regression/base/generic/trivial_min_unsat_core2.smt2.expected.out
new file mode 100644
index 000000000..832b8f1b3
--- /dev/null
+++ b/test/regression/base/generic/trivial_min_unsat_core2.smt2.expected.out
@@ -0,0 +1,2 @@
+unsat
+( a3 )
diff --git a/test/regression/base/generic/trivial_min_xor_unsat_core.smt2 b/test/regression/base/generic/trivial_min_xor_unsat_core.smt2
new file mode 100644
index 000000000..95b400270
--- /dev/null
+++ b/test/regression/base/generic/trivial_min_xor_unsat_core.smt2
@@ -0,0 +1,14 @@
+(set-option :produce-unsat-cores true)
+(set-option :minimal-unsat-cores true)
+
+(set-logic QF_UF)
+
+(declare-const b1 Bool)
+(declare-const b2 Bool)
+
+(assert (! (and b1 b2) :named a1))
+(assert (! (or b1 b2) :named a2))
+(assert (! (xor b1 b2) :named a3))
+
+(check-sat)
+(get-unsat-core)
diff --git a/test/regression/base/generic/trivial_min_xor_unsat_core.smt2.expected.err b/test/regression/base/generic/trivial_min_xor_unsat_core.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/regression/base/generic/trivial_min_xor_unsat_core.smt2.expected.out b/test/regression/base/generic/trivial_min_xor_unsat_core.smt2.expected.out
new file mode 100644
index 000000000..05da5c75d
--- /dev/null
+++ b/test/regression/base/generic/trivial_min_xor_unsat_core.smt2.expected.out
@@ -0,0 +1,2 @@
+unsat
+( a1 a3 )
diff --git a/test/unit/test_UnsatCore.cc b/test/unit/test_UnsatCore.cc
index 57df1dd16..c8df9097e 100644
--- a/test/unit/test_UnsatCore.cc
+++ b/test/unit/test_UnsatCore.cc
@@ -16,10 +16,29 @@
 
 namespace opensmt {
 
+bool isInCore(PTRef fla, vec<PTRef> const & coreTerms) {
+    return std::find(coreTerms.begin(), coreTerms.end(), fla) != coreTerms.end();
+}
+
 template <typename LogicT>
 class UnsatCoreTestBase {
 protected:
-    UnsatCoreTestBase(Logic_t type): logic{type} {}
+    UnsatCoreTestBase(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);
+        return {logic, config, "unsat_core"};
+    }
+};
+
+template <typename LogicT>
+class MinUnsatCoreTestBase {
+protected:
+    MinUnsatCoreTestBase(Logic_t type) : logic{type} {}
 
     LogicT logic;
     SMTConfig config;
@@ -27,14 +46,19 @@ class UnsatCoreTestBase {
     MainSolver makeSolver() {
         const char* msg = "ok";
         config.setOption(SMTConfig::o_produce_unsat_cores, SMTOption(true), msg);
+        config.setOption(SMTConfig::o_minimal_unsat_cores, SMTOption(true), msg);
         return {logic, config, "unsat_core"};
     }
 };
 
 /// Pure propositional and uninterpreted functions
-class UFUnsatCoreTest : public ::testing::Test, public UnsatCoreTestBase<Logic> {
+template <template<typename> typename TestBaseT>
+class UFUnsatCoreTestTp : public ::testing::Test, public TestBaseT<Logic> {
 protected:
-    UFUnsatCoreTest() : UnsatCoreTestBase(Logic_t::QF_UF) {}
+    using Base = TestBaseT<Logic>;
+    using Base::logic;
+
+    UFUnsatCoreTestTp() : Base(Logic_t::QF_UF) {}
     void SetUp() override {
         ufsort = logic.declareUninterpretedSort("U");
         x = logic.mkVar(ufsort, "x");
@@ -59,6 +83,9 @@ class UFUnsatCoreTest : public ::testing::Test, public UnsatCoreTestBase<Logic>
     SymRef f, g, p;
 };
 
+using UFUnsatCoreTest = UFUnsatCoreTestTp<UnsatCoreTestBase>;
+using MinUFUnsatCoreTest = UFUnsatCoreTestTp<MinUnsatCoreTestBase>;
+
 TEST_F(UFUnsatCoreTest, Bool_Simple) {
     MainSolver solver = makeSolver();
     solver.insertFormula(b1);
@@ -69,8 +96,77 @@ TEST_F(UFUnsatCoreTest, Bool_Simple) {
     auto core = solver.getUnsatCore();
     auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
-    EXPECT_TRUE(coreTerms[0] == b1 or coreTerms[1] == b1);
-    EXPECT_TRUE(coreTerms[0] == nb1 or coreTerms[1] == nb1);
+    EXPECT_TRUE(isInCore(b1, coreTerms));
+    EXPECT_TRUE(isInCore(nb1, coreTerms));
+}
+
+TEST_F(MinUFUnsatCoreTest, Min_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();
+    auto & coreTerms = core->getNamedTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(b1, coreTerms));
+    EXPECT_TRUE(isInCore(nb1, coreTerms));
+}
+
+TEST_F(MinUFUnsatCoreTest, Min_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->getNamedTerms();
+    ASSERT_EQ(coreTerms.size(), 1);
+    EXPECT_FALSE(isInCore(b1, coreTerms));
+    EXPECT_TRUE(isInCore(nb1, coreTerms));
+}
+
+TEST_F(MinUFUnsatCoreTest, Min_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->getNamedTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(b1, coreTerms));
+    EXPECT_TRUE(isInCore(nb1, coreTerms));
+}
+
+TEST_F(MinUFUnsatCoreTest, Min_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->getNamedTerms();
+    ASSERT_EQ(coreTerms.size(), 1);
+    EXPECT_TRUE(isInCore(b1, coreTerms));
+    EXPECT_FALSE(isInCore(nb1, coreTerms));
 }
 
 TEST_F(UFUnsatCoreTest, Bool_ReuseProofChain) {
@@ -94,8 +190,39 @@ TEST_F(UFUnsatCoreTest, Bool_ReuseProofChain) {
     auto core = solver.getUnsatCore();
     auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
-    EXPECT_TRUE(coreTerms[0] == a1 or coreTerms[1] == a1);
-    EXPECT_TRUE(coreTerms[0] == a2 or coreTerms[1] == a2);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_TRUE(isInCore(a2, coreTerms));
+    EXPECT_FALSE(isInCore(b4, coreTerms));
+}
+
+TEST_F(MinUFUnsatCoreTest, Min_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 & 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();
+    auto & coreTerms = core->getNamedTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_TRUE(isInCore(a2, coreTerms));
+    EXPECT_FALSE(isInCore(b4, coreTerms));
 }
 
 TEST_F(UFUnsatCoreTest, UF_Simple) {
@@ -114,14 +241,156 @@ TEST_F(UFUnsatCoreTest, UF_Simple) {
     auto core = solver.getUnsatCore();
     auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
-    EXPECT_TRUE(coreTerms[0] == a1 or coreTerms[1] == a1);
-    EXPECT_TRUE(coreTerms[0] == a3 or coreTerms[1] == a3);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_FALSE(isInCore(a2, coreTerms));
+    EXPECT_TRUE(isInCore(a3, coreTerms));
+}
+
+TEST_F(MinUFUnsatCoreTest, Min_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 & 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();
+    auto & coreTerms = core->getNamedTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_FALSE(isInCore(a2, coreTerms));
+    EXPECT_TRUE(isInCore(a3, coreTerms));
+}
+
+TEST_F(MinUFUnsatCoreTest, Min_UF_Simple_Unnamed1) {
+    // 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 & termNames = solver.getTermNames();
+    termNames.insert("a2", a2);
+    termNames.insert("a3", a3);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getNamedTerms();
+    ASSERT_EQ(coreTerms.size(), 1);
+    EXPECT_FALSE(isInCore(a1, coreTerms));
+    EXPECT_FALSE(isInCore(a2, coreTerms));
+    EXPECT_TRUE(isInCore(a3, coreTerms));
+}
+
+TEST_F(MinUFUnsatCoreTest, Min_UF_Simple_Unnamed2) {
+    // 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 & termNames = solver.getTermNames();
+    termNames.insert("a1", a1);
+    termNames.insert("a3", a3);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getNamedTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_FALSE(isInCore(a2, coreTerms));
+    EXPECT_TRUE(isInCore(a3, coreTerms));
+}
+
+TEST_F(MinUFUnsatCoreTest, Min_UF_Simple_Unnamed3) {
+    // 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 & termNames = solver.getTermNames();
+    termNames.insert("a1", a1);
+    termNames.insert("a2", a2);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    auto & coreTerms = core->getNamedTerms();
+    ASSERT_EQ(coreTerms.size(), 1);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_FALSE(isInCore(a2, coreTerms));
+    EXPECT_FALSE(isInCore(a3, coreTerms));
+}
+
+TEST_F(UFUnsatCoreTest, 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));
+}
+
+TEST_F(MinUFUnsatCoreTest, Min_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 & 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();
+    auto & coreTerms = core->getNamedTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_FALSE(isInCore(a1, coreTerms));
+    EXPECT_TRUE(isInCore(a2, coreTerms));
+    EXPECT_TRUE(isInCore(a3, coreTerms));
 }
 
 /// Pure arrays
-class AXUnsatCoreTest : public ::testing::Test, public UnsatCoreTestBase<Logic> {
+template <template<typename> typename TestBaseT>
+class AXUnsatCoreTestTp : public ::testing::Test, public TestBaseT<Logic> {
 protected:
-    AXUnsatCoreTest() : UnsatCoreTestBase(Logic_t::QF_AX) {}
+    using Base = TestBaseT<Logic>;
+    using Base::logic;
+
+    AXUnsatCoreTestTp() : Base(Logic_t::QF_AX) {}
     void SetUp() override {
         indexSort = logic.declareUninterpretedSort("Index");
         elementSort = logic.declareUninterpretedSort("Element");
@@ -138,6 +407,9 @@ class AXUnsatCoreTest : public ::testing::Test, public UnsatCoreTestBase<Logic>
     PTRef i, j, k, e, a;
 };
 
+using AXUnsatCoreTest = AXUnsatCoreTestTp<UnsatCoreTestBase>;
+using MinAXUnsatCoreTest = AXUnsatCoreTestTp<MinUnsatCoreTestBase>;
+
 TEST_F(AXUnsatCoreTest, AX_Simple) {
     // a1 := i != j
     // a2 := a[j] != a<i -> e>[j]
@@ -154,15 +426,45 @@ TEST_F(AXUnsatCoreTest, AX_Simple) {
     auto core = solver.getUnsatCore();
     auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
-    auto isInCore = [&](PTRef fla) -> bool { return std::find(coreTerms.begin(), coreTerms.end(), fla) != coreTerms.end(); };
-    EXPECT_TRUE(isInCore(a1));
-    EXPECT_TRUE(isInCore(a2));
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_TRUE(isInCore(a2, coreTerms));
+    EXPECT_FALSE(isInCore(a3, coreTerms));
+}
+
+TEST_F(AXUnsatCoreTest, Min_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 & 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();
+    auto & coreTerms = core->getNamedTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_TRUE(isInCore(a2, coreTerms));
+    EXPECT_FALSE(isInCore(a3, coreTerms));
 }
 
+
 /// Linear integer arithmetic
-class LIAUnsatCoreTest : public ::testing::Test, public UnsatCoreTestBase<ArithLogic> {
+template <template<typename> typename TestBaseT>
+class LIAUnsatCoreTestTp : public ::testing::Test, public TestBaseT<ArithLogic> {
 protected:
-    LIAUnsatCoreTest() : UnsatCoreTestBase(Logic_t::QF_LIA) {}
+    using Base = TestBaseT<ArithLogic>;
+    using Base::logic;
+
+    LIAUnsatCoreTestTp() : Base(Logic_t::QF_LIA) {}
     void SetUp() override {
         x = logic.mkIntVar("x");
         y = logic.mkIntVar("y");
@@ -182,6 +484,9 @@ class LIAUnsatCoreTest : public ::testing::Test, public UnsatCoreTestBase<ArithL
     PTRef nb1, nb2, nb3, nb4, nb5;
 };
 
+using LIAUnsatCoreTest = LIAUnsatCoreTestTp<UnsatCoreTestBase>;
+using MinLIAUnsatCoreTest = LIAUnsatCoreTestTp<MinUnsatCoreTestBase>;
+
 TEST_F(LIAUnsatCoreTest, LIA_Simple) {
     // a1 := x >= y
     // a2 := y >= z
@@ -201,16 +506,50 @@ TEST_F(LIAUnsatCoreTest, LIA_Simple) {
     auto core = solver.getUnsatCore();
     auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 3);
-    auto isInCore = [&](PTRef fla) -> bool { return std::find(coreTerms.begin(), coreTerms.end(), fla) != coreTerms.end(); };
-    EXPECT_TRUE(isInCore(a1));
-    EXPECT_TRUE(isInCore(a2));
-    EXPECT_TRUE(isInCore(a4));
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_TRUE(isInCore(a2, coreTerms));
+    EXPECT_FALSE(isInCore(a3, coreTerms));
+    EXPECT_TRUE(isInCore(a4, coreTerms));
+}
+
+TEST_F(LIAUnsatCoreTest, Min_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 & 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();
+    auto & coreTerms = core->getNamedTerms();
+    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));
 }
 
 /// Arrays + Linear integer arithmetic
-class ALIAUnsatCoreTest : public ::testing::Test, public UnsatCoreTestBase<ArithLogic> {
+template <template<typename> typename TestBaseT>
+class ALIAUnsatCoreTestTp : public ::testing::Test, public TestBaseT<ArithLogic> {
 protected:
-    ALIAUnsatCoreTest() : UnsatCoreTestBase(Logic_t::QF_ALIA) {}
+    using Base = TestBaseT<ArithLogic>;
+    using Base::logic;
+
+    ALIAUnsatCoreTestTp() : Base(Logic_t::QF_ALIA) {}
     void SetUp() override {
         intIntArraySort = logic.getArraySort(logic.getSort_int(), logic.getSort_int());
         arr1 = logic.mkVar(intIntArraySort, "a1");
@@ -235,6 +574,9 @@ class ALIAUnsatCoreTest : public ::testing::Test, public UnsatCoreTestBase<Arith
     PTRef nb1, nb2, nb3, nb4, nb5;
 };
 
+using ALIAUnsatCoreTest = ALIAUnsatCoreTestTp<UnsatCoreTestBase>;
+using MinALIAUnsatCoreTest = ALIAUnsatCoreTestTp<MinUnsatCoreTestBase>;
+
 TEST_F(ALIAUnsatCoreTest, ALIA_Simple) {
     // a1 := select(arr1, x) != select(arr1,y)
     // a2 := select(arr1, x) == 0
@@ -251,9 +593,34 @@ TEST_F(ALIAUnsatCoreTest, ALIA_Simple) {
     auto core = solver.getUnsatCore();
     auto & coreTerms = core->getTerms();
     ASSERT_EQ(coreTerms.size(), 2);
-    auto isInCore = [&](PTRef fla) -> bool { return std::find(coreTerms.begin(), coreTerms.end(), fla) != coreTerms.end(); };
-    EXPECT_TRUE(isInCore(a1));
-    EXPECT_TRUE(isInCore(a3));
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_FALSE(isInCore(a2, coreTerms));
+    EXPECT_TRUE(isInCore(a3, coreTerms));
+}
+
+TEST_F(ALIAUnsatCoreTest, Min_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 & 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();
+    auto & coreTerms = core->getNamedTerms();
+    ASSERT_EQ(coreTerms.size(), 2);
+    EXPECT_TRUE(isInCore(a1, coreTerms));
+    EXPECT_FALSE(isInCore(a2, coreTerms));
+    EXPECT_TRUE(isInCore(a3, coreTerms));
 }
 
 }