api: Fix kind documentation for BAG_MAKE. (#7663)

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 1c181988959b372daabf345d22e1f7c76285fb32..e6a03cbe445826ef6c583a40be106ad0d07cffcd 100644 (file)
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -2459,13 +2459,15 @@ enum Kind : int32_t
    */
   BAG_DUPLICATE_REMOVAL,
   /**
-   * The bag of the single element given as a parameter.
+   * Construct a bag with the given element and given multiplicity.
    *
    * Parameters:
-   *   - 1: Single element
+   *   - 1: The element
+   *   - 2: The multiplicity of the element. 
    *
    * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child) const`
+   *   - `Solver::mkTerm(Kind kind, const Term& child, const Term& child) const`
+   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
    */
   BAG_MAKE,
   /**

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index ba5bd655a6d6fbe7d929ba450c80c0d68ee7a356..cf6b29017a0ee6bc8ae87276018d82973a9ff4b8 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -659,6 +659,8 @@ TEST_F(TestApiBlackSolver, mkTerm)
 
   // mkTerm(Kind kind, Term child) const
   ASSERT_NO_THROW(d_solver.mkTerm(NOT, d_solver.mkTrue()));
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(BAG_MAKE, d_solver.mkTrue(), d_solver.mkInteger(1)));
   ASSERT_THROW(d_solver.mkTerm(NOT, Term()), CVC5ApiException);
   ASSERT_THROW(d_solver.mkTerm(NOT, a), CVC5ApiException);
   ASSERT_THROW(slv.mkTerm(NOT, d_solver.mkTrue()), CVC5ApiException);