Read the decimal element the loop selected

[HowardvanRooijen]

Fixes #55.

The defect

Inside the array element loop, every arm reads numValExpr - the element the loop selected with
MkSelect(arrVal, MkInt(i)). The Decimal arm did not. It called Eval a second time, on
subEnv.Expr, which is the array constant itself:

case TypeCode.Decimal:
    Expr val = EvaluateWithCompletion(model, subEnv.Expr ?? throw new ArgumentException(...));
    string numValue = ((RatNum)val).ToDecimalString(128);

What actually happens - the issue overstates one half and #64 overstates the other

The issue says every element gets the same wrong value or the cast fails outright. Measured, it
is always the cast: subEnv.Expr is an ArrayExpr, and no ArrayExpr is a RatNum. There is no
input that produces the same-value symptom - including with #64's sort mapping corrected locally, so
this is not #64 masking it.

#64 says this code is unreachable because a decimal[] never survives translation. That is true
only of a constraint naming a decimal constant, which is the shape #64 tested. Leave the elements
free and the theorem solves normally, and the element loop runs:

Shape	Before	After
decimal[], elements free	InvalidCastException: ... 'ArrayExpr' to type 'RatNum'	InvalidCastException: ... 'FPNum' to type 'RatNum'
List<decimal>, elements free	... 'ArrayExpr' ...	... 'FPNum' ...
decimal[], Values[0] == Values[1]	... 'ArrayExpr' ...	... 'FPNum' ...
decimal[], Values[0] == 1.5m	Z3Exception (#64)	Z3Exception (#64)

So #55 is observable, and the tests below observe it. What the fix changes is which expression the
cast rejects: after it, the decimal arm fails exactly where the float and double arms beside it
fail, on #64's floating-point range sort, rather than on a mistake of its own.

This reachability applies to the other element types too - float[], double[] and long[] with
free elements all reach marshalling and fail at their cast rather than in translation. That is #64's
territory, not this PR's, but it does make the remark added for #54's array arm in #80 imprecise, so
that remark is corrected here in the file this PR already edits.

The change

case TypeCode.Decimal:
    // Read the element the loop selected, not the array constant it was
    // selected from - every other arm here uses numValExpr. See #55.
    string numValue = ((RatNum)numValExpr).ToDecimalString(128);

Three lines below Theorem.cs:477 shift up by one; the four affected citations were checked against
their targets rather than shifted blindly, and one (Theorem.cs:654-699) was already off by a line
before this change.

Evidence that the fix is right, not just different

The tests can only assert on the failure, because #64 still declares a decimal array's range as a
floating-point sort. To check the fix actually produces correct values, #64's Decimal mapping was
corrected locally - IntSort domain, RealSort range, two sites - and the probe re-run. This
change is not in this PR; it is how the fix was verified.

Probe, with #64's decimal mapping corrected locally	#55 fixed	#55 reverted
Values[0] == 1.5m, Values[1] == 2.5m	1.5, 2.5	InvalidCastException
the same over a List<decimal>	1.5, 2.5	InvalidCastException
decimal[3], first two constrained	1.5, 2.5, 2.5	InvalidCastException
0.1m and decimal.MaxValue	0.1, 79228162514264337593543950335	InvalidCastException
elements free	0, 0	InvalidCastException

Each element takes its own value, at full decimal precision. That is the behaviour #55 asks for, and
it arrives the moment #64 stops standing in the way.

Tests

177 -> 180, all in CollectionSymbolTests.

Test	What it covers
Solve_DecimalArrayWithFreeElements_CastsTheElementNotTheArray	the fix itself: the cast rejects the element, not the array
Solve_DecimalListWithFreeElements_CastsTheElementNotTheArray	the generic-collection branch, which materialises its result through a constructor rather than ToArray and shares only the element read
Solve_DecimalArrayWithElementsConstrainedToEachOther_CastsTheElementNotTheArray	the loop is reached by a theorem that genuinely constrains the elements, not only by one that leaves them out

Each asserts two things, deliberately split: the message must not name an array - that is #55,
and it is what the fix changes - and it does name FPNum, which pins #64's sort mapping and
must be updated when #64 is fixed. These are the first message-based assertions in the suite; they
are here because the value cannot be asserted while #64 stands.

Three remarks were corrected rather than left to rot: the class remarks (failures split between
translation and marshalling depending on the constraint), the existing decimal[] pin (it is one
shape of #64, not proof of unreachability), and the float[] pin added by #80.

Mutation results

Mutation	Failures
Revert to EvaluateWithCompletion(model, subEnv.Expr)	3 - exactly the three new tests

The value-level mutations are the probe table above: with the sort mapping corrected, reverting the
fix turns every correct answer into an exception, so the tests are not merely pinning an exception
type that happens to have changed.

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors on
• 180/180 locally, 0.95s
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 76.7% -> 77.5% line (643 of 829), 69.6% -> 70.3% branch (442 of 628)

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.

[Copilot]

Pull request overview

This PR fixes a defect in ConvertZ3Expression’s collection element loop where the decimal arm evaluated/cast the array constant instead of the selected element expression, and adds characterization tests to ensure the correct expression is being cast (per #55) while keeping existing behavior pinned for #64.

Changes:

• Update TypeCode.Decimal array-element marshalling to read numValExpr (the selected element) rather than re-evaluating subEnv.Expr (the array constant).
• Add three tests that validate the decimal element loop now fails on the element expression (not the array) for free-element and constrained-element shapes, including the generic-collection branch.
• Refresh/realign test documentation line references and remarks to reflect current reachability and failure mode distinctions between translation vs marshalling.

Reviewed changes

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

File	Description
solutions/Z3.Linq/Theorem.cs	Fixes decimal element loop to use the selected element expression (numValExpr) consistently with other element types.
solutions/Z3.Linq.Tests/EnvironmentTypeTests.cs	Updates comment line references to match shifted line numbers in Theorem.cs.
solutions/Z3.Linq.Tests/CollectionSymbolTests.cs	Adjusts remarks around reachability/failure modes and adds new tests characterizing the #55 fix for decimal collections.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[github-actions]

Test Results

  1 files  ±0    1 suites  ±0   4s ⏱️ -2s
173 tests +3  173 ✅ +3  0 💤 ±0  0 ❌ ±0 
180 runs  +3  180 ✅ +3  0 💤 ±0  0 ❌ ±0 

Results for commit ba1fc74. ± Comparison against base commit 432653a.

♻️ This comment has been updated with latest results.