How to represent bottom element (integer domains) in SMT formula
First, you need to figure out the semantics of your language: does divide-by-zero cause the program to abort/halt/throw an exception, or does execution proceed and the divide-by-zero returns a NaN?
If it causes the program to halt, then you should not try to represent $\bot$ values.  Instead, treat division as a conditional statement, that first tests whether the divisor is zero, and if so, aborts/halts/etc.
If it returns a NaN, then one approach is to introduce an extra boolean variable associated with each program variable.  This boolean indicates whether the corresponding program variable holds a NaN.  You should be able to work out the appropriate constraints to ensure these boolean variables receive the appropriate values.