I'm writing a puzzle solver and i'm having some trouble implementing a rule where I have to count the number of elements of a particular state

i have a 2d grid of int symbols where their value corresponds to a particular entity which may occupy that cell. For example 1 = empty space, 2 = wall and so on.

I want to count the total number of walls in a column and assert that the sum MUST equal a constant value (i.e. the puzzle declares that column 0 has 5 walls so column 0 must have exactly 5 walls)

I'm using the following go bindings for z3

func (b *Board) checkcols() {
    for x := range BOARD_DIM {
        constname := fmt.Sprintf("col_%d_sum_%d", x, b.ColTotals[x])
        sum := b.ctx.IntConst(constname)
        for y := range BOARD_DIM {
            cond := address(x, y, &b.symbols).Eq(b.intToConst(int(Wall)))
            AddBoolToInt(&sum, &cond)
        }
        assertion := sum.Eq(b.intToConst(b.ColTotals[x]))
        log.Debug(assertion)
        b.slv.Assert(assertion)
    }
}

func AddBoolToInt(i *z3.Int, b *z3.Bool) {
    c := i.Context()
    bi := b.IfThenElse(c.FromInt(1, c.IntSort()), c.FromInt(0, c.IntSort()))
    tmp := i.Add(bi.(z3.Int))
    *i = tmp
}

on my test case (that i'll get to later) this will evaluate to something looking like the following examples

2025/03/23 15:19:08 DEBU (= (+ col_0_sum_1
      (ite (= 2 2) 1 0)
      (ite (= 2 2) 1 0)
      (ite (= 2 2) 1 0)
      (ite (= 2 2) 1 0)
      (ite (= 2 2) 1 0)
      (ite (= 2 2) 1 0)
      (ite (= 2 2) 1 0)
      (ite (= 2 2) 1 0))
   1)
2025/03/23 15:19:08 DEBU (= (+ col_1_sum_2
      (ite (= cell_1_0 2) 1 0)
      (ite (= cell_1_1 2) 1 0)
      (ite (= cell_1_2 2) 1 0)
      (ite (= cell_1_3 2) 1 0)
      (ite (= cell_1_4 2) 1 0)
      (ite (= cell_1_5 2) 1 0)
      (ite (= cell_1_6 2) 1 0)
      (ite (= cell_1_7 2) 1 0))
   2)

as you can see, i'm relying on ifthenelse to allow me to convert a boolean expression into an int so that I can conditionally add to my running total.

I wrote up a quick test case that I expect should be non satisfiable

 1 2 3 4 5 6 7 8 
0