From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 31 May 2022 21:03:31 +0000 (-0500)
Subject: Make subs minimize utility robust to non-constant evaluation (#8839)
X-Git-Tag: cvc5-1.0.1~82
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=04ceb6d3a1719e616c0e2bc28cbba89f83865f8f;p=cvc5.git

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 e0a107bf4..4af2a58e3 100644
--- 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 5dd9a3342..39d9d92bc 100644
--- 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
index 000000000..7ae20379c
--- /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)