SMT2 front-end: fix bvsmod semantics (sign follows divisor)

[tautschnig]

The SMT2 parser registered bvsmod identically to bvsrem, mapping both to mod_exprt — truncated division, where the remainder's sign follows the dividend. SMT-LIB defines bvsmod's result sign to follow the divisor: e.g. (bvsmod #b1111 #b0111) over 4 bits is 6 (−1 smod 7), not −1 (the existing code even noted "bvsmod doesn't [match]" without acting on it).

Consequence: wrong verdicts on benchmarks exercising bvsmod — e.g. SMT-LIB QF_BV/log-slicing/bvsmod_13.smt2 (:status unsat) was answered sat. Found by cross-solver differential testing on a stratified SMT-LIB 2024 sample; it was the only verdict disagreement in 3,426 runs.

bv_mod gains a sign_follows_divisor flag: bvsmod is computed from the truncated remainder r as (r != 0 && sign(r) != sign(t)) ? r + t : r, which matches the SMT-LIB definitional expansion case by case. The divisor-zero wrapper (bvsmod x 0 = x) is unchanged, as are bvsrem/bvurem.

Testing: new regression test regression/smt2_solver/bvsmod1 checks all 256 4-bit operand combinations against constants precomputed from the SMT-LIB definitional expansion; the definitional-expansion equivalence is also UNSAT at 13 bits; the full regression/smt2_solver suite passes.

• Each commit message has a non-empty body, explaining why the change was made.
• [n/a] 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).
• 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]

Pull request overview

Fixes CBMC’s SMT2 front-end handling of bvsmod to match SMT-LIB semantics, where the signed modulo result’s sign follows the divisor (as opposed to the truncated remainder semantics used by bvsrem, where the sign follows the dividend). This directly addresses incorrect SAT/UNSAT outcomes on benchmarks that use bvsmod.

Changes:

• Extend smt2_parsert::bv_mod with a sign_follows_divisor mode and implement SMT-LIB bvsmod as an adjustment of the truncated remainder r.
• Wire bvsmod to the new bv_mod(..., /*is_signed=*/true, /*sign_follows_divisor=*/true) behavior (keeping divisor-by-zero behavior unchanged).
• Add a regression test enumerating all 4-bit operand combinations to validate bvsmod semantics.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.

File	Description
src/solvers/smt2/smt2_parser.h	Extends bv_mod API with a sign_follows_divisor flag (defaulting to false).
src/solvers/smt2/smt2_parser.cpp	Implements divisor-sign-following bvsmod semantics and updates the bvsmod expression registration.
regression/smt2_solver/bvsmod1/test.desc	Adds a regression test spec expecting unsat for the exhaustive 4-bit check.
regression/smt2_solver/bvsmod1/bvsmod1.smt2	New SMT-LIB test that checks all 256 (4-bit) bvsmod pairs against precomputed expected results.

---

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

[kroening]

Is this worth introducing say smod_exprt?