From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 18 Jan 2022 19:55:54 +0000 (-0800)
Subject: [API] Add missing arity check (#7905)
X-Git-Tag: cvc5-1.0.0~530
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a1e130351e76d8af2773a45f099599da16287248;p=cvc5.git

[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 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<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 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()