Make subs minimize utility robust to non-constant evaluation (#8839)

Fixes #8834.

diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp
index e0a107bf463979146aa7e8d909284613e52d0928..4af2a58e30f14345873e0c8e3bd0c0e2f4939781 100644 (file)
--- a/src/theory/subs_minimize.cpp
+++ b/src/theory/subs_minimize.cpp
@@ -298,12 +298,16 @@ bool SubstitutionMinimize::findInternal(Node n,
       {
         // only recurse on relevant branch
         Node bval = value[cur[0]];
-        Assert(!bval.isNull() && bval.isConst());
-        unsigned cindex = bval.getConst<bool>() ? 1 : 2;
-        visit.push_back(cur[0]);
-        visit.push_back(cur[cindex]);
+        if (!bval.isNull() && bval.isConst())
+        {
+          unsigned cindex = bval.getConst<bool>() ? 1 : 2;
+          visit.push_back(cur[0]);
+          visit.push_back(cur[cindex]);
+          continue;
+        }
+        // otherwise, we handle it normally below
       }
-      else if (cur.getNumChildren() > 0)
+      if (cur.getNumChildren() > 0)
       {
         Kind ck = cur.getKind();
         bool alreadyJustified = false;

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 5dd9a3342ec0d87a4c000213635249712af88f04..39d9d92bc397d6a1ba8705501fdbfe4791775f52 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -755,6 +755,7 @@ set(regress_0_tests
   regress0/issue6738.smt2
   regress0/issue6741.smt2
   regress0/issue8807-model-core-partial.smt2
+  regress0/issue8834-model-core-nconst.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/issue8834-model-core-nconst.smt2 b/test/regress/cli/regress0/issue8834-model-core-nconst.smt2
new file mode 100644 (file)
index 0000000..7ae2037
--- /dev/null
+++ b/test/regress/cli/regress0/issue8834-model-core-nconst.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --model-cores=simple
+; EXPECT: sat
+(set-logic ALL)
+(assert (exists ((x Int)) (= (div 1 x x) 0)))
+(check-sat)