gistfile1.txt

; http://rise4fun.com/Z3/empty?frame=1&menu=0
(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(declare-fun c0 () (_ BitVec 32))
(declare-fun c1 () (_ BitVec 32))
(declare-fun c2 () (_ BitVec 32))
(declare-fun c3 () (_ BitVec 32))
(declare-fun c4 () (_ BitVec 32))
(declare-fun c5 () (_ BitVec 32))
(declare-fun c6 () (_ BitVec 32))
(assert (bvuge c0 #x00000020))
(assert (bvule c0 #x0000007E))
(assert (bvuge c1 #x00000020))
(assert (bvule c1 #x0000007E))
(assert (bvuge c2 #x00000020))
(assert (bvule c2 #x0000007E))
(assert (bvuge c3 #x00000020))
(assert (bvule c3 #x0000007E))
(assert (bvuge c4 #x00000020))
(assert (bvule c4 #x0000007E))
(assert (bvuge c5 #x00000020))
(assert (bvule c5 #x0000007E))
(assert (bvuge c6 #x00000020))
(assert (bvule c6 #x0000007E))
(assert (= #x82d7fada 
  (bvadd
    (bvmul #x140f0601 c0)
    (bvmul #x0a0a0501 c1)
    (bvmul #x04060401 c2)
    (bvmul #x01030301 c3)
    (bvmul #x00010201 c4)
    (bvmul #x00000101 c5)
    (bvmul #x00000001 c6)
)))
(check-sat)
(get-model)