multiplication is variadic (stanford-centaur#341)

This allows for creating multiplication-terms with more than two arguments.

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

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);