; COMMAND-LINE: --sygus-out=status --cegqi-si=none
; EXPECT: unsat

(set-logic BV)

(synth-fun f ((x (BitVec 32))) (BitVec 32))

(declare-var x (BitVec 32))
(constraint (= (bvor x #x00000001) (f x)))
(check-synth)