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
.