From 04ceb6d3a1719e616c0e2bc28cbba89f83865f8f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 31 May 2022 16:03:31 -0500 Subject: [PATCH] Make subs minimize utility robust to non-constant evaluation (#8839) Fixes #8834. --- src/theory/subs_minimize.cpp | 14 +++++++++----- test/regress/cli/CMakeLists.txt | 1 + .../cli/regress0/issue8834-model-core-nconst.smt2 | 5 +++++ 3 files changed, 15 insertions(+), 5 deletions(-) create mode 100644 test/regress/cli/regress0/issue8834-model-core-nconst.smt2 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() ? 1 : 2; - visit.push_back(cur[0]); - visit.push_back(cur[cindex]); + if (!bval.isNull() && bval.isConst()) + { + unsigned cindex = bval.getConst() ? 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) -- 2.30.2