[tautschnig]

When the shift operand and distance have different bit widths, the
incremental SMT2 backend extended them according to their type
signedness (extension_for_type). This is wrong for shifts: the shift
kind determines how the operand should be extended, and the distance
is always treated as unsigned.

Specifically:

• lshr of a signed operand was sign-extended (wrong: should zero-extend
  to avoid shifting sign bits into the result);
• ashr of an unsigned operand was zero-extended (wrong: should
  sign-extend to shift copies of the MSB into the result);
• A signed distance was sign-extended (wrong: shift distances are
  unsigned in the CBMC IR, per the SAT backend semantics).

Fix: always zero-extend the distance; extend the operand according to
the shift kind (sign-extend for ashr, zero-extend for lshr and shl).

The C front end only produces lshr for unsigned and ashr for signed
operands, so the default configuration is not affected. The bug affects
producers of GOTO programs that create shift expressions with the
"opposite" combination (e.g. lshr of a signed value).

Related to #9177/PR #9178 which fixes the same class of bug in the
non-incremental SMT2 backend.

Fixes #9362

Found by Jeroen Robben's specification-conformance pipeline (https://reports.robben.io/methodology/).

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing. Review the Copilot code review billing settings.

[kroening]

Same comment as in the other shift PR.