Drop the constraints that only existed to dodge #51

[HowardvanRooijen]

Stacked on #73, which fixes #51.

Why

Thirty-two tests carried a constraint - usually .Where(t => t.X2 == 0) - whose only purpose
was to keep the second symbol referenced, because an unreferenced one made Solve throw. They
were spread across six files and were actively misleading: a reader could not tell which
constraints belonged to a test's subject and which were there to work around a defect.

This is the cost of #51 made visible, and removing it is the last part of fixing it.

What it buys

The workarounds become regression coverage. With them gone, reverting the completion flag
fails 51 tests instead of 12 - the 32 removals expand to 39 extra cases through their
DataRows.

That is a better guarantee than any test I could write deliberately: the marshalling of every
supported type, the whole optimisation surface, and most of the documented throw sites now
exercise the free-symbol path as a side effect of testing what they were already testing.

Not mechanical

Removal was per-site, not a search-and-replace. A constraint stays wherever the test asserts
the value it pins - result.X2.ShouldBe(0) and friends - because dropping the constraint but
keeping the assertion would leave a test asserting a value on a now-free symbol, which is
exactly the flake the suite's determinism rule exists to prevent.

Kept for that reason: three tests in DistinctSelectorTheoremTests, one in RewriterTests,
two in DistinctInlineArrayTheoremTests, the multi-symbol tests in EnvironmentTypeTests
(where X2 == 2 is the subject, not a workaround), and SymbolsToString. Also kept:
Solve_EverySymbolConstrained_ReturnsResult, whose entire subject is that every symbol is
constrained.

One test that could not fail properly

Solve_DoubleSymbolUnderInvariantCulture_RoundTripsTheValue ran its solve on a bare Thread
with no try/catch. Once its workaround was removed, the mutation check made that solve
throw - and because the exception was unhandled on a background thread, it took down the test
host. The run reported:

Zero tests ran (782ms)
Exit code: -532462766
  Error output: Unhandled exception. System.InvalidCastException: ...

"Zero tests ran" rather than "one test failed" - which makes the mutation check above
unreadable, and would do the same to any future regression on that path. It now captures the
exception and asserts on it, exactly as its sibling pin already did.

Verification

• 145/145, unchanged count and unchanged assertions
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Mutation: 51 failures with the fix reverted, 0 with it in place

[Copilot]

Pull request overview

Removes workaround constraints in the test suite that existed solely to keep otherwise-unreferenced symbols mentioned (to avoid the pre-#51 Solve() crash), and updates one culture-thread test to capture exceptions so failures are reported cleanly instead of terminating the test host.

Changes:

• Removed incidental .Where(t => t.X2 == 0) / similar constraints from many tests so they now act as regression coverage for #51’s fix.
• Updated the invariant-culture dedicated-thread test to catch and surface exceptions instead of allowing an unhandled thread exception to abort the run.

Reviewed changes

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

Show a summary per file

File	Description
solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs	Drops incidental X2 constraints so unsupported-expression translation failures are tested without workaround noise.
solutions/Z3.Linq.Tests/TheoremCompositionTests.cs	Removes workaround constraints so basic composition/logging tests also cover unconstrained-symbol solving.
solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs	Removes workaround constraints from round-trip tests and adds exception capture on the invariant-culture thread to avoid host termination.
solutions/Z3.Linq.Tests/OptimizationTests.cs	Removes workaround constraints so optimization/orderby tests cover unconstrained symbols post-#51.
solutions/Z3.Linq.Tests/EnvironmentTypeTests.cs	Removes an incidental nested constraint so cross-nesting solve coverage also exercises unconstrained nested symbols.
solutions/Z3.Linq.Tests/DistinctSelectorTheoremTests.cs	Removes workaround constraint so distinct-selector tests cover unconstrained symbols post-#51.

---

💡 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    1 suites   4s ⏱️
142 tests 142 ✅ 0 💤 0 ❌
145 runs  145 ✅ 0 💤 0 ❌

Results for commit 445aad0.

♻️ This comment has been updated with latest results.