[Rafael-SOWNet]

x * floor(2/x) at 0 is 2 from each side, and the limit solver left it unevaluated. Every one-sided path put each factor's own limit in place of the factor, so each stopped at 0 * floor(+oo). The squeeze rule SolveAsBoundedTimesVanishing needs its other factor bounded, and floor(g) with g unbounded is not.

A new rule, SolveAsAStepOfAnUnboundedArgument, applies to a product or quotient with a factor floor(g), ceil(g) or round(g), where g is real-valued and the product f of the other factors contains x and tends to 0. Since |step(g) - g| <= 1, f * step(g) - f * g tends to 0, so the limit is lim f * g, for a value or an infinity alike. The rule answers only when that limit is not NaN. It is last in the list of solvers at +oo, so it covers one-sided limits at a finite point (through dest ± 1/x), limits at an infinity, and two-sided limits.

Input, at 0	side	2.6.0	master	this branch	true
x * floor(2/x)	L / R / both	0 / 0 / NaN	unevaluated	2	2
floor(1/x) * sin(x)	L / R / both	0 / 0 / NaN	unevaluated	1	1
x^2 * floor(1/x^2)	L / R / both	0 / 0 / 0	unevaluated	1	1
x * ceil(1/x)	L / R / both	0 / 0 / NaN	unevaluated	1	1
x * round(1/x)	L / R / both	throws OverflowException	unevaluated	1	1
-3 * x * floor(1/x)	L / R / both	0 / 0 / NaN	unevaluated	-3	-3
x^2 * floor(1/x)	L / R / both	0 / 0 / NaN	unevaluated	0	0
x * floor(1/x^2)	L / R / both	0 / 0 / NaN	unevaluated	-oo / +oo / NaN	-oo / +oo / none
sqrt(abs(x)) * floor(1/x)	L / R / both	unevaluated / unevaluated / NaN	unevaluated	-oo / +oo / NaN	-oo / +oo / none
x * floor(sin(1/x)/x)	L / R / both	0 / 0 / unevaluated	unevaluated	unevaluated	none
x * floor(2/x) + 3	both	unevaluated	unevaluated	5	5
floor(x) / x, at +oo		0	unevaluated	1	1
floor(2/x), sin(1/x)	both	NaN	NaN	NaN	none
floor(x)	both	unevaluated	NaN	NaN	none

Every true value was checked numerically at x = ±7/3·10^-k for k = 4..8. #2419's four rows, which master leaves unevaluated, are now answered, and its test pins floor(1/x) / floor(2/x) in their place. That limit is 1/2, which no rule here reaches yet, and 2.6.0 also leaves it unevaluated. Two limits that do not exist stay unevaluated rather than NaN, as on master: x * floor(sin(1/x)/x) and x * floor(1/x)^2.

Checked on this branch:

• Tests: UnitTests 19367 passed, plus the MCP, Terminal, InteractiveWrapper and F# wrapper suites, and the AOT smoke test.
• Harnesses: BoundCheck, RootCheck, CasBench, PropCheck, SimpSweep, RuleCheck, CanonCheck and Confluence all pass.
• limitcheck at DEPTH=3, COUNT=600, on 42 seeds against master: no row changed.

🤖 Generated with Claude Code

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 86.80%. Comparing base (2eea2e9) to head (1ea10ba).

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #2430      +/-   ##
==========================================
- Coverage   86.81%   86.80%   -0.02%     
==========================================
  Files         312      312              
  Lines       69551    69566      +15     
  Branches    20316    20323       +7     
==========================================
+ Hits        60383    60385       +2     
- Misses       4932     4946      +14     
+ Partials     4236     4235       -1     

Flag	Coverage Δ
cpp	37.77% <ø> (ø)
csharp	87.34% <100.00%> (-0.02%)	⬇️
fsharp	32.97% <ø> (ø)
interactive	39.81% <ø> (ø)

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

Files with missing lines	Coverage Δ
...nctions/Continuous/Limits/Solvers/Limit.Solvers.cs	88.26% <100.00%> (+0.91%)	⬆️
...ns/Continuous/Limits/Solvers/Solvers.Definition.cs	91.83% <100.00%> (-0.28%)	⬇️

... and 5 files with indirect coverage changes

🚀 New features to boost your workflow:

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