\(set-option :produce-models true\)
\(set-logic ALL\)
\(define-fun B0 \(\) Bool true\)
\(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
\(define-fun B1 \(\) Bool \(= |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
\(assert \(not \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
\(define-fun B2 \(\) Bool \(not false\)\)
\(assert B2\)
\(check-sat\)