(set-option :produce-models true)
; unsupported options
(set-option :config "verbosity=0")
(set-option :foo "bar")
(set-option :bar 0)
; declarations
(declare-const a (_ BitVec 4))
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Bool)
(assert (= a (! a :named x)))
(assert (= x #b1111))
(assert (! b :bar true))
(assert (! b :bar asdf))
(assert (! b :baz (bvadd a a)))
(assert (! (not c) :named y :baz (bvadd a a)))
(check-sat-assuming ((! (and c d) :foofoo g :named h)))
(get-value (a x b c y d))
(assert (! (or c d) :foofoo g :named z))
(assert (! (xor c d) :foofoo g :named gz :named zz))
(assert (! (and b y) :foo (bvnot a) :named by :bar zz))
(check-sat)
(get-value (a x b c y d z gz zz by))