Fix two defects in the solve-limits code found by review

[HowardvanRooijen]

Fixes two defects a code review of the stack found in the solve-limits work (#96), each verified
by measurement before fixing.

The two defects

A native Params leak. Z3Context.CreateLimits builds a Microsoft.Z3.Params - which is
IDisposable, backed by native memory - and Theorem.Check assigned it to the solver and dropped
it without disposing. Every Solve/Optimize that set a Timeout or ResourceLimit leaked one.
It is now a using, disposed when Check returns, by which point the solver has copied what it
needs.

A sub-millisecond timeout silently became no timeout. (uint)TimeSpan.FromMilliseconds(0.5).TotalMilliseconds
is 0, and Z3 reads timeout=0 as unlimited - so a caller who asked for a tiny timeout got none
and would hang on an undecidable theorem, exactly the failure the timeout was meant to prevent. The
value now rounds up (Math.Ceiling), so any positive timeout is at least one millisecond. Measured:
Timeout = 0.5ms on the sum-of-three-cubes theorem now throws TheoremUndecidedException in ~1ms
instead of running unbounded.

Verified, not a defect

The same review raised, at low confidence, that maximising an unsigned bit-vector might use signed
ordering. Measured and it does not: MkMaximize on a bit-vector is unsigned, so a uint symbol
constrained to [2e9, 3e9] maximises to 2999999999 and minimises to 2000000001 - both the
unsigned-correct extremes. No change needed; noted here so the finding is closed with evidence.

Not in scope (pre-existing / documented)

• The review noted the double/float read paths do not strip Z3's trailing ? for a
  non-terminating rational, unlike the decimal arms. That is on main unchanged, is open issue
  Circular decimal last char ‘?’ cannot parse decimal or double #6, and is already pinned by
  Solve_{Double,Float}SymbolWithANonTerminatingValue_ThrowsFormatException. Not a regression from
  this stack.
• It also noted that a conversion involving a bit-vector operand ((ulong)uintSymbol,
  (int)uintSymbol) throws NotImplementedException. That is the documented limitation from Support uint and ulong as bit-vector symbols #101 -
  mixing a bit-vector with a conversion is not supported - and it correctly refuses; the raw
  exception type is the pre-existing throw-site inconsistency, tracked separately.

Tests

321 -> 322: Solve_UndecidableTheoremWithASubMillisecondTimeout_StillThrows, guarded by
[Timeout] so a return to truncation fails the test rather than hanging. The leak fix is not
behaviourally testable - a leak fails no test - so it is verified by inspection (the using) and
the green suite; reverting the timeout fix fails the new test, reverting the using fails nothing,
as expected.

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors and
  documentation generation on
• 322/322 locally
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 88.5% -> 88.6% line (918 of 1036), branch unchanged at 78.2%

Release note

Releases remain on hold under #60 until Microsoft.Z3 5.x reaches nuget.org, so this reaches main
but not consumers. Nothing about the hold changes.

🤖 Generated with Claude Code

[github-actions]

Test Results

  1 files  ±0    1 suites  ±0   10s ⏱️ ±0s
309 tests +1  309 ✅ +1  0 💤 ±0  0 ❌ ±0 
322 runs  +1  322 ✅ +1  0 💤 ±0  0 ❌ ±0 

Results for commit d018cd2. ± Comparison against base commit eb2485f.