Skip to content

Instantly share code, notes, and snippets.

@jonnybest

jonnybest/get-proof-sample.smt2

Created November 19, 2012 21:14
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jonnybest/4113960 to your computer and use it in GitHub Desktop.
Save jonnybest/4113960 to your computer and use it in GitHub Desktop.
Download ZIP
An example of using the get-proof command for Z3
Raw
get-proof-sample.smt2
(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