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 /test | |
| 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 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/issue5550-num-children.smt2 | 6 |
2 files changed, 7 insertions, 0 deletions
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 |