[tlaplus] Existential quantifier over integers

I'm getting started with TLA+ and wrote a spec for a simple server that adds two integers: https://pastebin.com/Yc8qfwa7

When I run TLC, I get the following error:

The exception was a java.lang.RuntimeException

: TLC encountered a non-enumerable quantifier bound

Int.

line 46, col 34 to line 46, col 36 of module Addition

The error occurred when TLC was evaluating the nested

expressions at the following positions:

0. Line 46, column 3 to line 50, column 27 in Addition

1. Line 46, column 6 to line 49, column 84 in Addition

The errors refers to a "non-enumerable quantifier bound Int", but `Int` is an enumerable set.

The relevant snippet of my code reads

ServerResponse == \* server responds
/\ \E fromV \in CLIENT, aV \in Int, bV \in Int :
   /\ serverSt = [status |-> "processing", from |-> fromV, a |-> aV, b |-> bV]
   /\ serverSt' = "idle"
   /\ msgs' = msgs \cup {[type |-> "response", to |-> fromV, res |-> (aV + bV)]}
/\ UNCHANGED <<clientSt>>

What am I doing wrong here? And what's the idiomatic way to "deconstruct" records in TLA?

Thanks!

Abel