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

(synth-fun f ((x (_ BitVec 32))) (_ BitVec 32)
((Start (_ BitVec 32)) (StartBool Bool))
((Start (_ BitVec 32)
   (
             (bvudiv Start Start)
             (bvurem Start Start)
             (bvsdiv Start Start)
             #x00000001
             #x00000000
             #x00000002 x
             (ite StartBool Start Start)))
    (StartBool Bool (( bvult Start Start)
    			(bvugt Start Start)
    			(= Start Start)
             ))))
(declare-var x (_ BitVec 32) )

; property
(constraint (= (f #x00000008) #x00000004))
(constraint (= (f #x00000010) #x00000008))
(constraint (not (= (f x) #xffffffff)))


(check-synth)