Fix BigInt::div bugs and preclude aliasing via its interface

[tautschnig]

This PR fixes two long-standing bugs in the combined quotient/remainder method BigInt::div and then changes its interface so that argument aliasing — the source of one of the defect classes — becomes impossible to express.

1. Fix BigInt::div computing quotient from divisor instead of dividend. In the single-digit-divisor branch, the quotient was initialized from the divisor (q = y) instead of the dividend (q = x). As digit_div transforms the dividend in place into the quotient, any division of a dividend exceeding 64 bits by a divisor fitting a single 32-bit digit returned q = 1, r = 0. The bug dates back to the initial import; it went unnoticed because the only in-tree caller of BigInt::div is modinv, which itself has no callers, and the number.tst data never combines a >64-bit dividend with a single-digit divisor. Unit tests now cover that combination for all four sign combinations, a zero remainder, and the long-division branch.

2. Fix out-of-bounds read in BigInt::div when growing output operands. The general-division branch set the outputs' lengths before resizing them; resize copies length digits from the previous buffer, reading past its end whenever the result needed more digits than the output held. Results were unaffected, but the read is undefined behavior and flagged by address sanitizer. The existing tests masked this only because the test loop reuses output operands with previously grown buffers; the interface change in the next commit would expose it in every sanitizer run.

3. Make BigInt::div return its results, precluding aliasing. div wrote into caller-provided output arguments before it was done reading the inputs, so div(x, y, y, r) silently computed garbage, and passing the same object for quotient and remainder cannot have a valid result at all. Per our policy that aliasing must never be supported and should be excluded at compile time where possible, div now returns a BigInt::divisiont struct holding freshly constructed quotient and remainder — the aliasing cannot be written anymore. NRVO applies, so the non-aliased case pays nothing. The only in-tree caller (modinv) and the unit tests are updated.

• 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]

Pull request overview

Fixes a long-standing bug in the BigInt::div combined quotient/remainder implementation where (in the single-digit-divisor fast path) the quotient buffer was mistakenly initialised from the divisor instead of the dividend. This aligns the BigInt::div behaviour with the rest of the big-int division code paths (where the dividend’s digit array is the input that gets transformed into the quotient).

Changes:

• Fix BigInt::div single-digit-divisor branch to initialise q from x (dividend) so digit_div produces the correct quotient.
• Add a unit test that exercises the previously-uncovered case: dividend > 64 bits with a single-digit divisor, for both positive and negative dividends.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

File	Description
unit/big-int/big-int.cpp	Adds a regression unit test covering the >64-bit dividend + single-digit divisor BigInt::div path (including negative dividend semantics).
src/big-int/bigint.cc	Fixes quotient initialisation in BigInt::div so the single-digit-divisor fast path computes q from the dividend as intended.

---

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

[codecov]

Codecov Report

❌ Patch coverage is 87.75510% with 6 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.83%. Comparing base (ff8e112) to head (5bfb655).
⚠️ Report is 2 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/big-int/bigint-func.cc	0.00%	4 Missing ⚠️
src/big-int/bigint.cc	81.81%	2 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9121      +/-   ##
===========================================
+ Coverage    80.77%   80.83%   +0.05%     
===========================================
  Files         1712     1715       +3     
  Lines       189833   189982     +149     
  Branches        73       73              
===========================================
+ Hits        153347   153576     +229     
+ Misses       36486    36406      -80     

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