projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8994bc9) | patch
Use mkAnd where the number of children may be less than two. (#5551)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 3 Dec 2020 20:55:16 +0000 (21:55 +0100)
committerGitHub <noreply@github.com>
Thu, 3 Dec 2020 20:55:16 +0000 (14:55 -0600)
commitd92de1ce2d08ee4835a37b81e4139f1853eee909
treeba57ee49fedd0df3200e11e6132fc1b7b0587f0etree
parent8994bc9fd49a255286f8a6bac6c14407e8add41fcommit | 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 .
src/theory/uf/cardinality_extension.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/issue5550-num-children.smt2 [new file with mode: 0644] blob