SMT2: fix shift distance wider than the shifted operand

[kroening]

The SMT2 back-end (smt2_convt::convert_expr) brings the shift distance of
bvshl/bvlshr/bvashr to the width of the shifted operand, as required by
SMT-LIB. When the distance was wider than the operand it truncated the
distance with (_ extract (width_op0-1) 0).

This is unsound: a distance with high bits set is >= the operand width and
must shift the operand out entirely, but truncation drops exactly those bits.
For example, an 8-bit value shifted by a 16-bit distance of 256 was shifted
by 0 (since 256 mod 256 == 0) instead of being fully shifted out. This
disagreed with the boolbv (SAT) back-end, which computes the correct result.

Fix

When the distance is wider than the operand, perform the shift at the wider
distance width — zero-extending the operand (sign-extending for an arithmetic
right shift) — and extract the low width_op0 bits of the result. The
equal-width and narrower-distance cases are unchanged.

Testing

Adds unit tests to unit/solvers/smt2/smt2_conv.cpp pinning the generated
SMT2 for equal-width, narrower, and wider shift distances (lshr/shl/ashr).

Found via EBMC (diffblue/hw-cbmc): a SystemVerilog compound assignment
a >>= b with reg [7:0] a; reg [15:0] b = 256; was PROVED by the SAT backend
but REFUTED by z3/cvc5 because of this truncation.

Closes #9177

[codecov]

Codecov Report

❌ Patch coverage is 98.14815% with 1 line in your changes missing coverage. Please review.
✅ Project coverage is 80.86%. Comparing base (fd5dcee) to head (1fcfb06).
⚠️ Report is 8 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/solvers/smt2/smt2_conv.cpp	96.96%	1 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9178   +/-   ##
========================================
  Coverage    80.85%   80.86%           
========================================
  Files         1717     1717           
  Lines       190153   190193   +40     
  Branches        73       73           
========================================
+ Hits        153754   153800   +46     
+ Misses       36399    36393    -6     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.