cprover: only equate bit-compatible reads in axiom field-condition eval

[tautschnig]

What

axiomst::evaluate_fc() emitted, for every pair of same-state reads,

addresses_equal => *a == (a_type)*b

where the value is produced by typecast_exprt::conditional_cast. The solver
models that typecast_exprt as a value conversion, not a bitwise
reinterpretation, so the implication is not a true fact about memory whenever
the cast is not bit-preserving:

• reads of differing width (e.g. a 4-byte int and a 1-byte char at the
  same address);
• a 32-bit float vs a 32-bit int ((float)int_val converts numerically,
  e.g. (float)3 == 3.0f, rather than reinterpreting the bits);
• same-width aggregates vs scalars (the cast may not even be well-formed).

For those pairs the emitted equality over-constrains the formula and can rule
out genuine counterexamples, i.e. produce false proofs.

Change

Restrict the equality to pairs where (a_type)*b is a genuine bit-preserving
reinterpretation:

• identical read types (the cast is a no-op — this also covers reads
  differing only in signedness/qualifiers once they share a type), or
• both types are bit-vector-encoded scalars (signedbv/unsignedbv/bv/
  c_bool/c_enum/c_enum_tag) or pointers, and have equal,
  statically-known width (a two's-complement reinterpretation).

All other pairs (differing width, float/fixed-point, aggregates, or unknown
width for differing types) are skipped. Skipping a pair only ever removes a
constraint, so the change is sound.

Testing

This is a solver-internal soundness fix: the field-condition axioms are
emitted in the induction / counterexample-validation layer, and their effect
does not surface in the verification outcome of small standalone programs (I
confirmed that even equating the float/int and int/char pairs does not flip
the result of minimal reproducers). The skip/equate decisions were verified
directly by instrumenting evaluate_fc. regression/cprover passes
unchanged.

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

This PR tightens alias checking in axiomst::evaluate_fc by only equating pairs of evaluated addresses when their address expression types match, avoiding conditional casting between incompatible pointer types.

Changes:

• Add an early-continue to skip address pairs whose type() differs.
• Remove conditional_cast of b_it->address() to a_it->address().type() and compare original address expressions directly.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.69%. Comparing base (962c191) to head (459dcca).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9067   +/-   ##
========================================
  Coverage    80.68%   80.69%           
========================================
  Files         1714     1714           
  Lines       189522   189536   +14     
  Branches        73       73           
========================================
+ Hits        152925   152938   +13     
- Misses       36597    36598    +1     

☔ 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.