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 .

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index ddf81c2e8625c525834e662fafd94e35491cb0c9..3ea4c88e604fa8fa9810f901a3d74e73a061f313 100644 (file)
--- 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 4145c0e271471b097cc75e18bea847f8aaf95677..a401836f51f2eb4ca01df0e77be60feeb885b4b2 100644 (file)
--- 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 (file)
index 0000000..7581069
--- /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