From 4338d9d49a41022d34cd4cbabf17a66fdf39efae Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 23 May 2022 15:46:51 -0500
Subject: [PATCH] Make model core robust to when we cannot show the model
 satisfies input (#8811)

Fixes #8807.
---
 src/smt/model_core_builder.cpp                | 25 ++++++-------------
 src/theory/subs_minimize.cpp                  |  8 ++++++
 test/regress/cli/CMakeLists.txt               |  1 +
 .../issue8807-model-core-partial.smt2         |  6 +++++
 4 files changed, 23 insertions(+), 17 deletions(-)
 create mode 100644 test/regress/cli/regress0/issue8807-model-core-partial.smt2

diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp
index f2d84594b..8d784c2fc 100644
--- a/src/smt/model_core_builder.cpp
+++ b/src/smt/model_core_builder.cpp
@@ -79,36 +79,27 @@ bool ModelCoreBuilder::setModelCore(const std::vector<Node>& assertions,
   Trace("model-core") << "Minimizing substitution..." << std::endl;
   std::vector<Node> coreVars;
   std::vector<Node> impliedVars;
-  bool minimized = false;
   theory::SubstitutionMinimize sm(d_env);
   if (mode == options::ModelCoresMode::NON_IMPLIED)
   {
-    minimized = sm.findWithImplied(formula, vars, subs, coreVars, impliedVars);
+    sm.findWithImplied(formula, vars, subs, coreVars, impliedVars);
   }
   else if (mode == options::ModelCoresMode::SIMPLE)
   {
-    minimized = sm.find(formula, truen, vars, subs, coreVars);
+    sm.find(formula, truen, vars, subs, coreVars);
   }
   else
   {
     Unreachable() << "Unknown model cores mode";
   }
-  Assert(minimized)
-      << "cannot compute model core, since model does not satisfy input!";
-  if (minimized)
-  {
-    m->setUsingModelCore();
-    Trace("model-core") << "...got core vars : " << coreVars << std::endl;
+  m->setUsingModelCore();
+  Trace("model-core") << "...got core vars : " << coreVars << std::endl;
 
-    for (const Node& cv : coreVars)
-    {
-      m->recordModelCoreSymbol(cv);
-    }
-    return true;
+  for (const Node& cv : coreVars)
+  {
+    m->recordModelCoreSymbol(cv);
   }
-  Trace("model-core") << "...failed, model does not satisfy input!"
-                      << std::endl;
-  return false;
+  return true;
 }
 
 }  // namespace cvc5::internal
diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp
index 96e5c9b17..e0a107bf4 100644
--- a/src/theory/subs_minimize.cpp
+++ b/src/theory/subs_minimize.cpp
@@ -258,6 +258,14 @@ bool SubstitutionMinimize::findInternal(Node n,
   if (value[n] != target)
   {
     Trace("subs-min") << "... not equal to target " << target << std::endl;
+    // depends on all variables
+    for (const std::pair<const TNode, Node>& v : value)
+    {
+      if (v.first.isVar())
+      {
+        reqVars.push_back(v.first);
+      }
+    }
     return false;
   }
 
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 24d311604..5156d97df 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -753,6 +753,7 @@ set(regress_0_tests
   regress0/issue6605-2-abd-triv.smt2
   regress0/issue6738.smt2
   regress0/issue6741.smt2
+  regress0/issue8807-model-core-partial.smt2
   regress0/ite_arith.smt2
   regress0/ite_real_int_type.smtv1.smt2
   regress0/ite_real_valid.smtv1.smt2
diff --git a/test/regress/cli/regress0/issue8807-model-core-partial.smt2 b/test/regress/cli/regress0/issue8807-model-core-partial.smt2
new file mode 100644
index 000000000..4daaf2cff
--- /dev/null
+++ b/test/regress/cli/regress0/issue8807-model-core-partial.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --model-cores=simple -q
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () (Bag String)) 
+(assert (= (bag.choose a) "")) 
+(check-sat)
-- 
2.30.2