diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-12-03 21:55:16 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-03 14:55:16 -0600 |
| commit | d92de1ce2d08ee4835a37b81e4139f1853eee909 (patch) | |
| tree | ba57ee49fedd0df3200e11e6132fc1b7b0587f0e /src/theory | |
| parent | 8994bc9fd49a255286f8a6bac6c14407e8add41f (diff) | |
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 .
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/uf/cardinality_extension.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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; |