support muli-ary multiplication in the SMT2 front-end

This adds support for muli-ary multiplication to the SMT2 front-end.

Author: polgreen

regression/smt2_solver/basic-bv1/basic-bv1.smt2

@@ -14,9 +14,13 @@
 (define-fun b09 () Bool (= (bvlshr #xf0 #x03) #x1e)) ; unsigned (logical) shift right
 (define-fun b10 () Bool (= (bvashr #xf0 #x03) #xfe)) ; signed (arithmetical) shift right#x0a
 
+; Multi-ary variants, where applicable
+(define-fun b11 () Bool (= (bvadd #x07 #x03 #x01) #x0b)) ; addition
+(define-fun b12 () Bool (= (bvmul #x07 #x03 #x01) #x15)) ; multiplication
+
 ; rotation
-(define-fun b11 () Bool (= ((_ rotate_left 2) #xf7) #xdf)) ; rotation left
-(define-fun b12 () Bool (= ((_ rotate_right 2) #x07) #xc1)) ; rotation right
+(define-fun b13 () Bool (= ((_ rotate_left 2) #xf7) #xdf)) ; rotation left
+(define-fun b14 () Bool (= ((_ rotate_right 2) #x07) #xc1)) ; rotation right
 
 ; Bitwise Operations
 
@@ -63,7 +67,7 @@
 ; all must be true
 
 (assert (not (and
-  b01 b02 b03 b04 b05 b06 b07 b08 b09 b10 b11 b12
+  b01 b02 b03 b04 b05 b06 b07 b08 b09 b10 b11 b12 b13 b14
   d01
   power-test
   p1 p2 p3 p4 p5 p6 p7 p8)))

src/solvers/smt2/smt2_parser.cpp

@@ -1034,8 +1034,8 @@ void smt2_parsert::setup_expressions()
   expressions["bvadd"] = [this] { return multi_ary(ID_plus, operands()); };
   expressions["+"] = [this] { return multi_ary(ID_plus, operands()); };
   expressions["bvsub"] = [this] { return binary(ID_minus, operands()); };
-  expressions["bvmul"] = [this] { return binary(ID_mult, operands()); };
-  expressions["*"] = [this] { return binary(ID_mult, operands()); };
+  expressions["bvmul"] = [this] { return multi_ary(ID_mult, operands()); };
+  expressions["*"] = [this] { return multi_ary(ID_mult, operands()); };
 
   expressions["-"] = [this] {
     auto op = operands();