Splitting the state on sign-extentions uses the same code that was used initially only for CMOVE splitting. This causes the reasoner to mark as "secret-dependent CMOVEs" also simple sign-extentions of the secret.
Fix:
[ ] Split handling of sign-extentions and CMOVEs in the scanner
Splitting the state on sign-extentions uses the same code that was used initially only for CMOVE splitting. This causes the reasoner to mark as "secret-dependent CMOVEs" also simple sign-extentions of the secret.
Fix: