[Rafael-SOWNet]

Happypig375 on #2183: "Some solutions like { a ^ 2 provided a > -5 and a >= 0 } obviously needs improvement - the conditions can be merged." Here a >= 0 forces a > -5, so the condition is a >= 0.

When Providedf joins conditions, and in a condition written as a conjunction, a conjunct that another conjunct of the same condition forces is now dropped. PredicateEntailment decides that for comparisons against numbers. A conjunct stated twice forces itself, so this covers the repeated condition #2183 dropped as well. Of two that force each other, the first is kept, and the conjunction is rebuilt only where something goes, so every other condition keeps its shape.

Input	Was (2.6.0)	Now
(sqrt(x) = a) provided a > -5, solved	{ a ^ 2 provided a > -5 } (... and a >= 0 on master)	{ a ^ 2 provided a >= 0 }
x provided a > 1 and a > 2	x provided a > 1 and a > 2	x provided a > 2
(x provided a > 0) provided a >= 0	x provided a >= 0 and a > 0	x provided a > 0

x provided a > 0 and b > 0 and x provided a > 0 and a < 5 keep both conjuncts, in the order written. The rows are in #2183's breaking entry, which is not released yet.

Measured

• Suite: 17,324 passed, 0 failed, 13 skipped.
• Intbench chain against master 4fe3219: identical on every family, 0 moves. Performance gate passed on all 19 gated benchmarks.
• Harnesses: BoundCheck 0 disagreements, RootCheck 596/596, CasBench 120/121 with 0 wrong, SimpSweep 10463/10463, CrashCheck 0 crashed, PropCheck and RuleCheck clean, CanonCheck (2091) and Confluence (3) matching their baselines.

Part of #212.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 86.46%. Comparing base (4fe3219) to head (b5cd798).
⚠️ Report is 1 commits behind head on master.

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #2186      +/-   ##
==========================================
+ Coverage   86.45%   86.46%   +0.01%     
==========================================
  Files         297      297              
  Lines       65448    65455       +7     
  Branches    19215    19218       +3     
==========================================
+ Hits        56582    56595      +13     
+ Misses       4808     4804       -4     
+ Partials     4058     4056       -2     

Flag	Coverage Δ
cpp	37.77% <ø> (ø)
csharp	87.03% <100.00%> (+0.01%)	⬆️
fsharp	32.97% <ø> (ø)
interactive	40.72% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

Files with missing lines	Coverage Δ
...luation/Evaluation.Omni/Evaluation.Omni.Classes.cs	89.15% <100.00%> (+0.20%)	⬆️

... and 4 files with indirect coverage changes

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.