Guard conflict-analysis walks over prevboundval_ against running past the chain start - #3193
Closed
EamonHetherton wants to merge 1 commit into
Closed
Guard conflict-analysis walks over prevboundval_ against running past the chain start#3193EamonHetherton wants to merge 1 commit into
EamonHetherton wants to merge 1 commit into
Conversation
… the chain start
ConflictSet walks a column's bound-change history backwards through
prevboundval_[pos] in eight places, all of the form
while (relaxUb >= localdom.prevboundval_[locdomchg.pos].first)
locdomchg.pos = localdom.prevboundval_[locdomchg.pos].second;
The chain terminates with .second == -1 at the column's first change.
All eight walks assumed the terminal is unreachable: the four
bound-relaxation walks in resolveLinearLeq/resolveLinearGeq had no
guard, and the four in explainInfeasibilityConflict/
explainBoundChangeConflict noted "pos should never become -1" and
backed it with only an assert. The assumed invariant is numeric and
breaks under extreme proof constraints (observed with a proof rhs of
8e-08 at mip_feasibility_tolerance 1e-9 on a model whose coefficients
span 13 orders of magnitude): pos becomes -1, the loop reads
prevboundval_[-1], and then chases the garbage index it finds there
through arbitrary heap memory until it faults.
Observed as intermittent production SIGSEGVs with two distinct crash
sites in the same solve: directly inside resolveLinearLeq (core dump
at the loop above), and later in explainBoundChange indexing
conflictPoolPropagation with a reason read through a garbage stack
position deposited by a walk that happened to survive.
The relaxation walks now stop at the chain's first entry, keeping that
entry in the explanation - a valid, conservative superset. The
explanation walks now report the bound change as unexplainable so the
optional conflict cut is skipped.
Fixes ERGO-Code#3190
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## latest #3193 +/- ##
=======================================
Coverage 72.92% 72.93%
=======================================
Files 436 436
Lines 106038 106094 +56
Branches 17071 17078 +7
=======================================
+ Hits 77329 77375 +46
- Misses 28433 28443 +10
Partials 276 276 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Member
|
When you get around to looking at #3190, @fwesselm and @Opt-Mucca, perhaps this fix is correct. As an AI-generated fix, we can't accept it as it is. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #3190.
The eight backward walks over a column's bound-change chain assumed the chain terminal (predecessor position -1) is unreachable. The invariant is numeric and can break, after which the walk reads prevboundval_[-1] and chases garbage indices. The relaxation walks now stop at the chain's first entry, which stays in the explanation as a valid superset; the assert-guarded walks now report the bound change as unexplainable so the optional conflict cut is skipped.
🤖 Generated with Claude Code