Populate symbols the solver leaves uninterpreted

[HowardvanRooijen]

Fixes #51.

The defect

Solve() threw whenever the environment declared a symbol the model did not interpret:

using var ctx = new Z3Context();
ctx.NewTheorem<Symbols<int, int>>().Where(t => t.X1 == 1).Solve();
// System.InvalidCastException: Unable to cast object of type 'Microsoft.Z3.IntExpr'
// to type 'Microsoft.Z3.IntNum'   at Theorem.cs:516

A Z3 model is partial: it assigns values only to the constants the solver actually needed.
Model.Eval(Expr t, bool completion = false) therefore hands back an uninterpreted constant as
itself, and the cast fails.

The condition is not "no constraint mentions it". A constraint the solver discards as it is
asserted leaves its symbol uninterpreted just the same - measured:

Query	Before	After
where t.X1 > 0	{X1 = 1, X2 = 0}	unchanged
where t.X1 == t.X1	InvalidCastException	{X1 = 0, X2 = 0}
where t.X1 > 0 || t.X1 <= 0	InvalidCastException	{X1 = 0, X2 = 0}

That is why the fix is model completion rather than an inspection of the constraint list.

The change

Four lines, plus one helper. All four evaluation sites now route through
EvaluateWithCompletion, so the invariant is stated and enforced in one place rather than
repeated four times - which is how the omission came to exist at all.

The helper is appended at the end of the class so that no existing line moves: the test
suite cites Theorem.cs:NNN in 23 places and every one of them stays accurate.

Measured, per type

Symbols<T, int> with only X2 constrained:

	Before	After
int / long / DateTime	InvalidCastException (IntExpr→IntNum)	populated
double / decimal	InvalidCastException (RealExpr→RatNum)	populated
string	Z3Exception: expression is not a string literal	populated ("")
bool	passed - silently false	populated
short / float	InvalidCastException	ArgumentException - #63 / #54, uncovered not caused

Two things worth calling out. string failed differently from everything else, because it is
read with Expr.String rather than a cast. And bool never failed at all - Expr.IsTrue is
false for any term that is not literally true, so a free bool silently returned false
whether or not the model said anything about it. That is the quiet half of this defect and the
reason it survived so long.

short and float still fail, at the reflection write rather than at evaluation. Those are
#63 and #54, which this fix uncovers rather than causes. Their pins are unchanged.

Tests

133 → 145. Two pins rewritten from "throws" to the fixed behaviour; twelve added, one per
distinct code path. No test asserts a free symbol's value - it is arbitrary by definition, and
Dependabot bumps Microsoft.Z3 daily here.

Mutation results

Reverting the flag fails exactly the 12 intended tests and nothing else. Per site, inlining a
plain Eval at one site at a time:

Site	Path	Tests that fail
445	array element	1
507	scalar, nested, Optimize, OrderBy	10
634	anonymous type	1
471	decimal array	0

1 + 10 + 1 = 12, a clean partition: every test is bound to exactly one site.

Site 471 has no coverage, and cannot have any. A decimal[] fails during translation
(#64), so the line is unreachable - CollectionSymbolTests pins exactly that. It is changed
for consistency, not because anything can observe it. Reverting it alone fails no test, which
is expected rather than an oversight.

Two of the twelve new tests are deliberately not mutation-sensitive and say so in their
doc comments: the free bool case (which always worked) and the partially-constrained array
(free elements resolve through the array's else-value, so they were never independently
arbitrary). They are there for the semantics they record.

Nothing was masked. All 131 pre-existing tests pass identically with completion on and
off, which is the evidence that completion only fills gaps and never overrides a value the
solver chose.

Deliberately out of scope

#52-#58, #63, #64 all stay documented-not-fixed with their pins green. Site 471 keeps its
existing wrong argument - it evaluates the whole array rather than the selected element, which
is #55.

One new issue raised: #75. Routing the sites through a helper turned an unguarded null at site
634 into a CS8604 build error. The helper takes Expr? so this PR changes no behaviour there;
#75 tracks the underlying inconsistency and the reachable NullReferenceException it causes.

Trade-off worth stating

Today a constraint that silently fails to apply - a rewriter that drops one, a Where that
never got composed - surfaces loudly as an exception. After this it surfaces as 0, false or
"". That is inherent to the requested semantics, so Solve and Optimize now document that
a free symbol's value is arbitrary and must not be read as a solved one.

It also makes #57 easier to hit: a satisfiable theorem over a value-type environment with free
symbols now returns all-zeros, which is exactly what an unsatisfiable one returns. That argues
for #57 being the next one fixed.

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors on
• 145/145 in ~1.5s
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage unchanged at 75.8% line / 69.3% branch. The new tests exercise arms that were
  already covered by line count, so this change buys behaviour, not coverage.

Releases remain on hold under #60, so this ships to main but not to consumers.

[Copilot]

Pull request overview

This PR addresses Z3’s partial model behavior by ensuring that solution marshalling always evaluates symbols with model completion enabled, preventing InvalidCastException (and similar) when the model does not interpret a symbol (e.g., unconstrained symbols or symbols only present in tautologies simplified away).

Changes:

• Routes all model evaluation through a single EvaluateWithCompletion helper that calls model.Eval(..., completion: true).
• Updates public API XML remarks for Solve() / Optimize() to clarify behavior for free symbols.
• Replaces “known defect” tests with assertions that solving/optimizing succeeds while only constrained values are asserted; adds additional regression coverage (tautology case, optimization path, anonymous/nested env, arrays, several scalar types).

Reviewed changes

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

Show a summary per file

File	Description
solutions/Z3.Linq/Theorem{T}.cs	Adds XML remarks documenting that unconstrained/free symbols take arbitrary values.
solutions/Z3.Linq/Theorem.cs	Centralizes model evaluation via EvaluateWithCompletion and updates all evaluation sites to use completion.
solutions/Z3.Linq.Tests/TheoremSolveTests.cs	Updates #51 repro tests to expect successful solve; adds tautology-only mention coverage.
solutions/Z3.Linq.Tests/TheoremCompositionTests.cs	Updates line-number citation in remarks.
solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs	Adds regression tests for unconstrained symbols across multiple scalar types.
solutions/Z3.Linq.Tests/OptimizationTests.cs	Adds regression coverage for unconstrained symbols in optimization and query-syntax orderby.
solutions/Z3.Linq.Tests/EnvironmentTypeTests.cs	Adds coverage for anonymous and nested environments with unconstrained properties.
solutions/Z3.Linq.Tests/CollectionSymbolTests.cs	Adds coverage for unconstrained array elements and mixed constrained/free element behavior.

---

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

[HowardvanRooijen]

The diagnosis is right, and better than the comment realises: this null is not hypothetical. An anonymous environment holding a nested object reaches it, because GetEnvironment gives a nested environment a null Expr:

ctx.NewTheorem(new { inner = new Leaf(), n = default(int) }).Where(t => t.n == 1).Solve();
// System.NullReferenceException

I verified that and raised it as #75.

Not guarding it here is deliberate, for two reasons.

The first is scope. This PR fixes #51 and changes nothing else, which is what makes its mutation matrix a clean partition - reverting one call site fails exactly the tests bound to it. Adding a guard would change observable behaviour for a shape unrelated to model completion.

The second is that a guard is the worse fix. Two lines further on, the branch already throws NotSupportedException naming the property, for every type that is not bool or int - a nested object included. It never gets there because the evaluation happens first. So the right fix is to move that type check above the evaluation, not to add a fourth ArgumentException. #75 says so.

One correction: this does not trigger nullable-analysis warnings - the build is clean with TreatWarningsAsErrors on. It did produce CS8604 when I first wrote the helper with a non-nullable parameter, and that is exactly how the defect was found.

See the reply on the helper for why the parameter stays nullable.

[HowardvanRooijen]

The doc inconsistency is a fair hit and is now fixed - the XML remarks state the null contract explicitly.

The signature stays Expr?, though, because it is the accurate one. The helper genuinely can receive null today: Environment.Expr is Expr?, and the anonymous-type branch at line 634 passes it unguarded, unlike the three sites in ConvertZ3Expression. That is reachable, not theoretical - see the other reply and #75.

Given that, a non-nullable parameter has only two implementations, and both are worse:

• subEnv.Expr! at the call site - a suppression that asserts something untrue, and the only one in the file.
• a guard in the helper or at line 634 - changes behaviour for a case this PR is not about, and pre-empts the better fix Anonymous environment with a nested object property throws NullReferenceException #75 proposes (move the property-type check above the evaluation, so the NotSupportedException that already exists two lines later fires and names the property).

So Expr? describes what the code does rather than what we wish it did, and the remarks now say why, where the next reader will look.

On "model.Eval does not accept null" - true at runtime, but worth being precise: Microsoft.Z3 carries no nullable annotations at all, so the compiler permits it either way. That obliviousness is why the missing guard survived; it is not something the signature here can enforce.

Happy to flip this if you would rather the PR carried the guard - it is a judgement call about scope, not a disagreement about the facts.

[github-actions]

Test Results

  1 files  ± 0    1 suites  ±0   3s ⏱️ ±0s
142 tests +12  142 ✅ +12  0 💤 ±0  0 ❌ ±0 
145 runs  +12  145 ✅ +12  0 💤 ±0  0 ❌ ±0 

Results for commit ca34b7f. ± Comparison against base commit 5c017e2.