Initializing non-deterministic variables in QBF

Question

I'm trying to translate the following pseudocode to QBF. The integers are encoded as simple fixed-width bitvectors, and the entire procedure runs in polynomial space ensuring QBF has enough representational power for a compact formula.

The following formula is nested to a linear depth in n, producing 2^n increments when unrolled. Using QBF allows for an exponentially more compact encoding than SAT. QBF solvers can typically handle thousands of variables, SAT solvers handle millions. For even modest values of n, such as n=30, unrolling to SAT would produce billions of variables (impractical), while a QBF encoding would be extremely practical with only tens of variables.

counter = 0
for loop_aux_0 in {0,1}:
  for loop_aux_1 in {0,1}:
    for loop_aux_2 in {0,1}:
      .
        .
          .
            for loop_aux_n in {0,1}: 
              counter += f(loop_aux_0, loop_aux_1, .., loop_aux_n)
assert(counter > 0)

Here f is an arbitrary function that outputs 0 or 1.

This suggests a QBF implementation (although missing initialization) utilizing an adder circuit with its output fed back in as input:

∃ counter[n] ∀ loop_aux[n] ∃ f_output[1] (counter += f_output) & (f_output == f(loop_aux_0, loop_aux_1, .., loop_aux_n))

How can I add clauses or auxiliary variables to simulate sequential counter initialization?