I've been looking into how to use the z3 theorem prover in Haskell lib. It turns out to be not very well documented, and my particular use case did not have any example programs available.
Specifically, for the abstract value representation for my analysis I want to be able to represent integer values as a unique identifier, along with some constraints that are found by learning about the control flow of the program. For example a binding for within an if statement's then branch where the condition is should add the constraint that the abstract value that flows to that binding has a value greater than 0. This should be combined with finding other constants, such as using an integer to generating a list of a constant size or count down to a specific value. Finally we'd like to use Z3 to be able to prove that a value is within some concrete integer range. Using this information we can optimize the storage and arithmetic of these values statically, and omit a bunch of runtime checks that handle arbitrary precision integers.