How to represent bottom element (integer domains) in SMT formula

Question

I'm doing some work with static analysis and need to represent local variables as SMT formulas. In general this is fairly straight forward, depending on the domain of the static analysis. However, my question lies when needing to represent impossible or infeasible values, e.g., divide by zero paths from the static analysis under an integer domain. This is often referred to as the bottom element, ⊥.

I'm struggling to develop a formula which can represent these "impossible" (integer) values. Is there a way to do this?

I've been thinking along the lines as an impossible inequality, but I've been unsuccessful thus far. Similarly, I've thought about attempting to represent using divide by zero within an SMT formula, such as the following Z3/SMT formula:

(declare-const a Int)
(assert (= (/ a 0.0) 1.0))
(assert (= (/ a 0.0) 2.0))
(check-sat)

However, given the application, I'm not sure this is going to be helpful.

Application: I'm using this to compare results between two different static analyses between different domains.

tl;dr:

How to represent infeasible, bottom integer elements as SMT formula?

Edit

I didn't try this enough, maybe the question is more along the lines of "is there a more eloquent way to model a bottom value besides the following?":

(declare-const a Int)
(assert (and (>= a 0) (< a 0)))
(check-sat)

The above will yield unsat, as expected. And since I'm trying to compare results of different static analyses, I can formulate questions about locals as such (is a top value equal to a bottom value):

(declare-const a Int)
(declare-const b Int)
(assert (= (and (>= a 0) (< a 0))
           (or (>= b 0) (< b 0))))

(check-sat)

This will also yield unsat.

Answer 1

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.