[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.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index e3d70bde5759b765419d9901a694e7970aef62fc..458dd359aba6aed8dbd343f30b042ff8402b8dba 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5216,6 +5216,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& 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 70331803c6b3c523edc002cee51471371e586dc3..1d0f1f2768ab2995b3d14564a72196ce3cb9262c 100644 (file)
--- 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 (file)
index 0000000..1962c53
--- /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 519b81a4022bd5effb7d664cf68a587262898c17..3c0c974e2acc5d0f37f1f79d1aa768c282b333f6 100755 (executable)
--- 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()