How to convert a sum and product constraint into SMT-lib2

Question

I'm wondering what the best way to convert a sum a le

$$\sum_{v=exprLB}^{exprUB} 2 + exprContent(v) = 12.34$$

or similarly a product

$$\prod_{v=exprLB}^{exprUB} exprContent(v) = 1234$$

into an SMT-lib2 expression, specifically for solving with Z3 (or even metitarski).

I thought there would be an obvious approach with a quantifier, but I'm having trouble creating it, and in many use cases such a sum is likely to have constants for $exprLB$ and $exprUB$, which would mean that I would hope some kind of tactic would simply unroll it into a long sequence of addition, where use of a quantifier might make that much more difficult.

For example, a fairly trivial tactic to convert

$$\sum_{i=1}^{3} \dfrac {2} x_{i} = 12$$

into

$$2 / x_{1} + 2 / x_{2} + 2 / x_{3}$$

which is both trivially expressed as (and trivially solved by most SMT solvers) as

(+ 
  (/ 2 x1)
  (/ 2 x2)
  (/ 2 x3)
)

yielding

sat (model (define-fun x1 () Real 1.0) (define-fun x2 () Real 1.0) (define-fun x3 () Real (/ 1.0 4.0)) )

How can I generally express a sum over three expressions (lower-bound, upper-bound, and accumulator) elegantly in smt-lib2?