From 61ff06a688f9e0d71e081c02f7cf2456932e240e Mon Sep 17 00:00:00 2001
From: ffrohn <florian.frohn@cs.rwth-aachen.de>
Date: Tue, 12 Dec 2023 09:23:22 +0100
Subject: [PATCH] multiplication is variadic (#341)

This allows for creating multiplication-terms with more than two arguments.
---
 include/ops.h      |  2 +-
 tests/test-int.cpp | 21 +++++++++++++++++++++
 2 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/include/ops.h b/include/ops.h
index eb33bef2e..9b45e539c 100644
--- a/include/ops.h
+++ b/include/ops.h
@@ -196,7 +196,7 @@ namespace std
 namespace smt {
 // ops that can be applied to n arguments
 const std::unordered_set<PrimOp> variadic_ops(
-    { And, Or, Xor, Plus, BVAnd, BVOr, BVAdd });
+    { And, Or, Xor, Plus, Mult, BVAnd, BVOr, BVAdd });
 
 bool is_variadic(PrimOp po);
 }  // namespace smt
diff --git a/tests/test-int.cpp b/tests/test-int.cpp
index 55d6f0baa..a1ac9ec48 100644
--- a/tests/test-int.cpp
+++ b/tests/test-int.cpp
@@ -41,6 +41,27 @@ class IntTests : public ::testing::Test,
   Sort intsort;
 };
 
+// test for creating variadic mult-terms
+TEST_P(IntTests, Mult)
+{
+  Term two = s->make_term(2, intsort);
+  Term three = s->make_term(3, intsort);
+  Term four = s->make_term(4, intsort);
+  Term twentyfour = s->make_term(24, intsort);
+  Term mult;
+  try
+  {
+    mult = s->make_term(Mult, {two, three, four});
+  }
+  catch (const IncorrectUsageException &e)
+  {
+    FAIL() <<  "creating mult-term failed: " << e.what();
+  }
+  s->assert_formula(s->make_term(Equal, twentyfour, mult));
+  auto res = s->check_sat();
+  assert(res.is_sat());
+}
+
 TEST_P(IntTests, IntDiv)
 {
   Term five = s->make_term(5, intsort);