From 445aad0c38327597fb1ff14356963885e7996961 Mon Sep 17 00:00:00 2001 From: Howard van Rooijen Date: Tue, 1 Sep 2026 17:03:45 +0100 Subject: [PATCH] Drop the constraints that only existed to dodge #51 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. With #51 fixed they are noise, and they were actively misleading: a reader could not tell which constraints were part of a test's subject and which were there to work around a defect. Removing them turns those tests into regression coverage for the fix. Reverting the completion flag now fails 51 tests rather than 12. Constraints whose value a test actually asserts are kept - the point stands only where the symbol was genuinely incidental. Also captures the exception on the invariant-culture thread. That solve ran on a bare Thread with no try/catch, so an exception there was unhandled and killed the test host: the run reported "zero tests ran" instead of one failure, which made the mutation check above impossible to read. Its sibling pin already did this. Co-Authored-By: Claude Opus 5 (1M context) --- .../DistinctSelectorTheoremTests.cs | 1 - .../Z3.Linq.Tests/EnvironmentTypeTests.cs | 1 - solutions/Z3.Linq.Tests/OptimizationTests.cs | 29 +++++--------- .../SymbolTypeMarshallingTests.cs | 39 ++++++++++--------- .../Z3.Linq.Tests/TheoremCompositionTests.cs | 5 +-- .../UnsupportedExpressionTests.cs | 10 ++--- 6 files changed, 33 insertions(+), 52 deletions(-) diff --git a/solutions/Z3.Linq.Tests/DistinctSelectorTheoremTests.cs b/solutions/Z3.Linq.Tests/DistinctSelectorTheoremTests.cs index f8d4229..e1b8679 100644 --- a/solutions/Z3.Linq.Tests/DistinctSelectorTheoremTests.cs +++ b/solutions/Z3.Linq.Tests/DistinctSelectorTheoremTests.cs @@ -118,7 +118,6 @@ public void Distinct_SelectorOverDistinctMultipliers_Solves(int first, int secon var result = (from t in context.NewTheorem>() where Z3Methods.Distinct(multipliers.Select(m => t.X1 * m).ToArray()) where t.X1 > 0 - where t.X2 == 0 select t).Solve(); // Assert diff --git a/solutions/Z3.Linq.Tests/EnvironmentTypeTests.cs b/solutions/Z3.Linq.Tests/EnvironmentTypeTests.cs index 26cb271..16704d6 100644 --- a/solutions/Z3.Linq.Tests/EnvironmentTypeTests.cs +++ b/solutions/Z3.Linq.Tests/EnvironmentTypeTests.cs @@ -234,7 +234,6 @@ public void Solve_NestedObjectEnvironment_ConstrainsAcrossNestingLevels() var result = context.NewTheorem() .Where(t => t.Inner.A == t.Top * 2) .Where(t => t.Top == 5) - .Where(t => t.Inner.B == 0) .Solve(); // Assert diff --git a/solutions/Z3.Linq.Tests/OptimizationTests.cs b/solutions/Z3.Linq.Tests/OptimizationTests.cs index dfe9ee9..bdffed7 100644 --- a/solutions/Z3.Linq.Tests/OptimizationTests.cs +++ b/solutions/Z3.Linq.Tests/OptimizationTests.cs @@ -31,7 +31,6 @@ public void Optimize_Minimize_ReturnsTheSmallestSatisfyingValue() var result = context.NewTheorem>() .Where(t => t.X1 >= 5) .Where(t => t.X1 <= 9) - .Where(t => t.X2 == 0) .Optimize(Optimization.Minimize, t => t.X1); // Assert @@ -49,7 +48,6 @@ public void Optimize_Maximize_ReturnsTheLargestSatisfyingValue() var result = context.NewTheorem>() .Where(t => t.X1 >= 5) .Where(t => t.X1 <= 9) - .Where(t => t.X2 == 0) .Optimize(Optimization.Maximize, t => t.X1); // Assert @@ -66,8 +64,7 @@ public void Optimize_MinimizeAndMaximizeOverTheSameTheorem_ReturnOppositeBounds( using var context = new Z3Context(); var theorem = context.NewTheorem>() .Where(t => t.X1 >= 5) - .Where(t => t.X1 <= 9) - .Where(t => t.X2 == 0); + .Where(t => t.X1 <= 9); // Act var minimum = theorem.Optimize(Optimization.Minimize, t => t.X1); @@ -87,8 +84,7 @@ public void OrderBy_ProducesTheSameResultAsMinimize() using var context = new Z3Context(); var theorem = context.NewTheorem>() .Where(t => t.X1 >= 3) - .Where(t => t.X1 <= 8) - .Where(t => t.X2 == 0); + .Where(t => t.X1 <= 8); // Act var viaOptimize = theorem.Optimize(Optimization.Minimize, t => t.X1); @@ -107,8 +103,7 @@ public void OrderByDescending_ProducesTheSameResultAsMaximize() using var context = new Z3Context(); var theorem = context.NewTheorem>() .Where(t => t.X1 >= 3) - .Where(t => t.X1 <= 8) - .Where(t => t.X2 == 0); + .Where(t => t.X1 <= 8); // Act var viaOptimize = theorem.Optimize(Optimization.Maximize, t => t.X1); @@ -129,8 +124,7 @@ public void OrderBy_BeforeSolveIsCalled_DoesNotSolveAnything() using var log = new StringWriter(); using var context = new Z3Context { Log = log }; var theorem = context.NewTheorem>() - .Where(t => t.X1 >= 3) - .Where(t => t.X2 == 0); + .Where(t => t.X1 >= 3); // Act var deferred = theorem.OrderBy(t => t.X1); @@ -150,8 +144,7 @@ public void OrderByDescending_BeforeSolveIsCalled_DoesNotSolveAnything() using var log = new StringWriter(); using var context = new Z3Context { Log = log }; var theorem = context.NewTheorem>() - .Where(t => t.X1 >= 3) - .Where(t => t.X2 == 0); + .Where(t => t.X1 >= 3); // Act var deferred = theorem.OrderByDescending(t => t.X1); @@ -223,8 +216,7 @@ public void Optimize_MinimizingIsNotJustTheFirstSatisfyingModel() using var context = new Z3Context(); var theorem = context.NewTheorem>() .Where(t => t.X1 >= 5) - .Where(t => t.X1 <= 100) - .Where(t => t.X2 == 0); + .Where(t => t.X1 <= 100); // Act var minimised = theorem.Optimize(Optimization.Minimize, t => t.X1); @@ -243,8 +235,7 @@ public void Optimize_CalledTwiceOnTheSameTheorem_LeavesItReusable() using var context = new Z3Context(); var theorem = context.NewTheorem>() .Where(t => t.X1 >= 1) - .Where(t => t.X1 <= 4) - .Where(t => t.X2 == 0); + .Where(t => t.X1 <= 4); // Act var first = theorem.Optimize(Optimization.Minimize, t => t.X1); @@ -267,8 +258,7 @@ public void Optimize_WithUnrecognisedDirection_ThrowsArgumentOutOfRangeException // than defaulting to one of them (Theorem.cs:118). using var context = new Z3Context(); var theorem = context.NewTheorem>() - .Where(t => t.X1 == 1) - .Where(t => t.X2 == 0); + .Where(t => t.X1 == 1); // Act & Assert Should.Throw( @@ -329,8 +319,7 @@ public void Optimize_AfterAdditionalWhere_RespectsTheNarrowedConstraints() using var context = new Z3Context(); var parent = context.NewTheorem>() .Where(t => t.X1 >= 1) - .Where(t => t.X1 <= 10) - .Where(t => t.X2 == 0); + .Where(t => t.X1 <= 10); var child = parent.Where(t => t.X1 >= 6); // Act diff --git a/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs b/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs index 98605d5..600a2cb 100644 --- a/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs +++ b/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs @@ -43,7 +43,6 @@ public void Solve_IntSymbol_RoundTripsTheValue(int value) // Act var result = context.NewTheorem>() .Where(t => t.X1 == value) - .Where(t => t.X2 == 0) .Solve(); // Assert @@ -65,7 +64,6 @@ public void Solve_LongSymbol_RoundTripsTheValue(long value) // Act var result = context.NewTheorem>() .Where(t => t.X1 == value) - .Where(t => t.X2 == 0) .Solve(); // Assert @@ -84,7 +82,6 @@ public void Solve_BoolSymbol_RoundTripsTheValue(bool value) // Act var result = context.NewTheorem>() .Where(t => t.X1 == value) - .Where(t => t.X2 == 0) .Solve(); // Assert @@ -106,7 +103,6 @@ public void Solve_DoubleSymbol_RoundTripsTheValue(double value) // Act var result = context.NewTheorem>() .Where(t => t.X1 == value) - .Where(t => t.X2 == 0) .Solve(); // Assert @@ -125,7 +121,6 @@ public void Solve_DecimalSymbol_RoundTripsTheValue() // Act var result = context.NewTheorem>() .Where(t => t.X1 == Value) - .Where(t => t.X2 == 0) .Solve(); // Assert @@ -145,7 +140,6 @@ public void Solve_StringSymbol_RoundTripsTheValue(string value) // Act var result = context.NewTheorem>() .Where(t => t.X1 == value) - .Where(t => t.X2 == 0) .Solve(); // Assert @@ -165,7 +159,6 @@ public void Solve_DoubleSymbolWithInequality_SatisfiesTheConstraint() var result = context.NewTheorem>() .Where(t => t.X1 > 10.5) .Where(t => t.X1 < 11.0) - .Where(t => t.X2 == 0) .Solve(); // Assert @@ -190,8 +183,7 @@ public void Solve_ShortSymbol_ThrowsInvalidCastException() // Arrange using var context = new Z3Context(); var theorem = context.NewTheorem>() - .Where(t => t.X1 == 7) - .Where(t => t.X2 == 1); + .Where(t => t.X1 == 7); // Act & Assert Should.Throw(() => theorem.Solve()); @@ -212,8 +204,7 @@ public void Solve_FloatSymbol_ThrowsArgumentException() // Arrange using var context = new Z3Context(); var theorem = context.NewTheorem>() - .Where(t => t.X1 == 1.5f) - .Where(t => t.X2 == 0); + .Where(t => t.X1 == 1.5f); // Act & Assert Should.Throw(() => theorem.Solve()); @@ -240,7 +231,6 @@ public void Solve_DateTimeSymbol_ReturnsTheSameInstantAsLocalTime() // Act var result = context.NewTheorem>() .Where(t => t.X1 == utc) - .Where(t => t.X2 == 0) .Solve(); // Assert @@ -309,7 +299,6 @@ public void Solve_DoubleSymbolUnderCommaDecimalCulture_ThrowsZ3ParserError() using var context = new Z3Context(); _ = context.NewTheorem>() .Where(t => t.X1 == 1.5) - .Where(t => t.X2 == 0) .Solve(); } catch (Exception ex) @@ -337,18 +326,29 @@ public void Solve_DoubleSymbolUnderInvariantCulture_RoundTripsTheValue() // that the two differ only by culture. This is what the defect above should look like // once it is fixed. double? value = null; + Exception? captured = null; var thread = new Thread(() => { CultureInfo.CurrentCulture = CultureInfo.InvariantCulture; - using var context = new Z3Context(); - var result = context.NewTheorem>() - .Where(t => t.X1 == 1.5) - .Where(t => t.X2 == 0) - .Solve(); + try + { + using var context = new Z3Context(); + var result = context.NewTheorem>() + .Where(t => t.X1 == 1.5) + .Solve(); - value = result?.X1; + value = result?.X1; + } + catch (Exception ex) + { + // Captured rather than left to escape: an exception on a bare thread is + // unhandled, so it takes down the test host and the run reports "zero tests + // ran" rather than one failed test. The pin above already does this; this + // counterpart did not, because it was not expected to throw. + captured = ex; + } }); // Act @@ -356,6 +356,7 @@ public void Solve_DoubleSymbolUnderInvariantCulture_RoundTripsTheValue() thread.Join(SolveTimeout).ShouldBeTrue("the solve on the invariant-culture thread did not finish"); // Assert + captured.ShouldBeNull(); value.ShouldBe(1.5); } diff --git a/solutions/Z3.Linq.Tests/TheoremCompositionTests.cs b/solutions/Z3.Linq.Tests/TheoremCompositionTests.cs index a3da268..99cc59f 100644 --- a/solutions/Z3.Linq.Tests/TheoremCompositionTests.cs +++ b/solutions/Z3.Linq.Tests/TheoremCompositionTests.cs @@ -68,8 +68,7 @@ public void Where_OriginalTheorem_RemainsIndependentlySolvable() // child's extra constraint did not leak backwards. using var context = new Z3Context(); var parent = context.NewTheorem>() - .Where(t => t.X1 == 3) - .Where(t => t.X2 == 0); + .Where(t => t.X1 == 3); var child = parent.Where(t => t.X1 == 4); // Act @@ -137,7 +136,6 @@ public void Log_WhenNotSet_SolvingDoesNotThrow() // Act var result = (from t in context.NewTheorem>() where t.X1 == 1 - where t.X2 == 0 select t).Solve(); // Assert @@ -159,7 +157,6 @@ public void Dispose_CalledOnContext_LeavesTheContextUsable() var result = (from t in context.NewTheorem>() where t.X1 == 11 - where t.X2 == 0 select t).Solve(); // Assert diff --git a/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs b/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs index bceb51d..1fb7f49 100644 --- a/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs +++ b/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs @@ -38,8 +38,7 @@ public void Solve_ConditionalExpression_ThrowsNotSupportedException() // express if-then-else, so this is a gap rather than a fundamental limit. using var context = new Z3Context(); var theorem = context.NewTheorem>() - .Where(t => (t.X1 > 0 ? t.X1 : 0) == 1) - .Where(t => t.X2 == 0); + .Where(t => (t.X1 > 0 ? t.X1 : 0) == 1); // Act & Assert Should.Throw(() => theorem.Solve()); @@ -54,8 +53,7 @@ public void Solve_CallToAnUnrecognisedMethod_ThrowsNotSupportedException() // (ExpressionVisitor.cs:277). using var context = new Z3Context(); var theorem = context.NewTheorem>() - .Where(t => Increment(t.X1) == 2) - .Where(t => t.X2 == 0); + .Where(t => Increment(t.X1) == 2); // Act & Assert Should.Throw(() => theorem.Solve()); @@ -70,8 +68,7 @@ public void Solve_UnsupportedCast_ThrowsNotImplementedException() // than NotSupportedException - the throw sites are not consistent about which they use. using var context = new Z3Context(); var theorem = context.NewTheorem>() - .Where(t => (long)t.X1 == 1L) - .Where(t => t.X2 == 0); + .Where(t => (long)t.X1 == 1L); // Act & Assert Should.Throw(() => theorem.Solve()); @@ -162,7 +159,6 @@ public void Solve_SupportedExpressionsAlongsideRejectedOnes_StillRejects() using var context = new Z3Context(); var theorem = context.NewTheorem>() .Where(t => t.X1 > 0) - .Where(t => t.X2 == 0) .Where(t => (t.X1 > 5 ? t.X1 : 0) == 6); // Act & Assert