Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
An example of using the get-proof command for Z3
(set-option :produce-proofs true)
(declare-const a Int)
(assert (and (> a 3) (< a 2)))
(check-sat)
(get-proof)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment