; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic BV)

(define-fun bit-reset ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32)
  (let ((modulo-shift (BitVec 32) (bvand bit #x0000001f)))
	 (bvand modulo-shift x)))

(synth-fun btr ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32)
    ((Start (BitVec 32) (
                         (Constant (BitVec 32))
                         (Variable (BitVec 32))
			 (bvneg  Start) (bvnot  Start) (bvadd  Start Start) (bvand  Start Start) (bvlshr Start Start) (bvmul  Start Start) (bvor   Start Start) (bvshl  Start Start)
                         ))))

(declare-var x   (BitVec 32))
(declare-var bit (BitVec 32))
(constraint (= (btr x bit) #b00000000000000000000000000000000))

(check-synth)