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

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))

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.


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