From a1e130351e76d8af2773a45f099599da16287248 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 18 Jan 2022 11:55:54 -0800 Subject: [PATCH] [API] Add missing arity check (#7905) Fixes #7894. The API was not performing an arity check for associative operators with less than two children. This commit adds the missing check. --- src/api/cpp/cvc5.cpp | 1 + test/regress/CMakeLists.txt | 1 + .../regress0/parser/issue7894-parse-error-assoc.smt2 | 6 ++++++ test/regress/run_regression.py | 3 ++- 4 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/parser/issue7894-parse-error-assoc.smt2 diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index e3d70bde5..458dd359a 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5216,6 +5216,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const else if (kind::isAssociative(k)) { // associative case, same as above + checkMkTerm(kind, children.size()); res = d_nodeMgr->mkAssociative(k, echildren); } else diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 70331803c..1d0f1f276 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -813,6 +813,7 @@ set(regress_0_tests regress0/parser/issue6908-get-value-uc.smt2 regress0/parser/issue7274.smt2 regress0/parser/issue7860-parse-only-reset.smt2 + regress0/parser/issue7894-parse-error-assoc.smt2 regress0/parser/linear_arithmetic_err1.smt2 regress0/parser/linear_arithmetic_err2.smt2 regress0/parser/linear_arithmetic_err3.smt2 diff --git a/test/regress/regress0/parser/issue7894-parse-error-assoc.smt2 b/test/regress/regress0/parser/issue7894-parse-error-assoc.smt2 new file mode 100644 index 000000000..1962c53e1 --- /dev/null +++ b/test/regress/regress0/parser/issue7894-parse-error-assoc.smt2 @@ -0,0 +1,6 @@ +; DISABLE-TESTER: dump +; COMMAND-LINE: -q +; SCRUBBER: grep -o "must have at least 2 children" +; EXPECT: must have at least 2 children +; EXIT: 1 +(assert (= (+ 0))) diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 519b81a40..3c0c974e2 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -551,7 +551,8 @@ def run_regression( if disable_tester not in g_testers: print("Unknown tester: {}".format(disable_tester)) return EXIT_FAILURE - testers.remove(disable_tester) + if disable_tester in testers: + testers.remove(disable_tester) expected_output = expected_output.strip() expected_error = expected_error.strip() -- 2.30.2