Skip to content

Instantly share code, notes, and snippets.

@ashiato45
Created April 9, 2019 05:28
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save ashiato45/f23e6378130c847cfb220244a4e3be61 to your computer and use it in GitHub Desktop.
(set-logic QF_BV)
(set-option :produce-models true)
(declare-const x (_ BitVec 3))
(declare-const y (_ BitVec 3))
(define-fun A0 () Bool (bvule (bvadd x y) (_ bv3 3))) ; the number 3 in the bitvector of width 3
(assert A0)
(check-sat)
(get-model)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment