From d92de1ce2d08ee4835a37b81e4139f1853eee909 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 3 Dec 2020 21:55:16 +0100 Subject: [PATCH] Use mkAnd where the number of children may be less than two. (#5551) An AND was constructed from a vector that may only hold a single or no element. This PR uses mkAnd instead. Fixes #5550 . --- src/theory/uf/cardinality_extension.cpp | 3 ++- test/regress/CMakeLists.txt | 1 + test/regress/regress0/issue5550-num-children.smt2 | 6 ++++++ 3 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/issue5550-num-children.smt2 diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index ddf81c2e8..3ea4c88e6 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1175,7 +1175,8 @@ bool SortModel::checkLastCall() } } Node cl = getCardinalityLiteral( d_maxNegCard ); - Node lem = NodeManager::currentNM()->mkNode( OR, cl, NodeManager::currentNM()->mkNode( AND, force_cl ) ); + Node lem = NodeManager::currentNM()->mkNode( + OR, cl, NodeManager::currentNM()->mkAnd(force_cl)); Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl; d_im.lemma(lem, LemmaProperty::NONE, false); return false; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4145c0e27..a401836f5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -592,6 +592,7 @@ set(regress_0_tests regress0/issue5144-resetAssertions.smt2 regress0/issue5540-2-dump-model.smt2 regress0/issue5540-model-decls.smt2 + regress0/issue5550-num-children.smt2 regress0/ite.cvc regress0/ite2.smt2 regress0/ite3.smt2 diff --git a/test/regress/regress0/issue5550-num-children.smt2 b/test/regress/regress0/issue5550-num-children.smt2 new file mode 100644 index 000000000..75810699b --- /dev/null +++ b/test/regress/regress0/issue5550-num-children.smt2 @@ -0,0 +1,6 @@ +; EXPECT: sat +(set-logic UFC) +(declare-sort a 0) +(declare-fun b () a) +(assert (not (fmf.card b 1))) +(check-sat) \ No newline at end of file -- 2.30.2