Je veux OF = 0

(assert (= (ite (= ((_ extract 63 0) SymVar_0) (_ bv1 64)) ((_ extract 0 0) (bvxor (bvashr ((_ extract 63 0) SymVar_0) (bvsub ((_ extract 63 0) SymVar_0) (_ bv1 64))) (bvashr ((_ extract 63 0) SymVar_0) (bvsub ((_ extract 63 0) SymVar_0) (_ bv2 64))))) (_ bv0 1)) (_ bv0 1)))

{'SymVar_0': 562949953421312}


=================================

Je veux OF = 1

(assert (= (ite (= ((_ extract 63 0) SymVar_0) (_ bv1 64)) ((_ extract 0 0) (bvxor (bvashr ((_ extract 63 0) SymVar_0) (bvsub ((_ extract 63 0) SymVar_0) (_ bv1 64))) (bvashr ((_ extract 63 0) SymVar_0) (bvsub ((_ extract 63 0) SymVar_0) (_ bv2 64))))) (_ bv0 1)) (_ bv1 1)))

{'SymVar_0': 1}