Skip to content

fix(smt): spell a divergence's values in the check engine's order whichever copy the solver gave which #2168

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
devin-ai-integration wants to merge 2 commits into from
Open

fix(smt): spell a divergence's values in the check engine's order whichever copy the solver gave which #2168

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c41ec80
fix(smt): spell a divergence's values in the check engine's order whi…
devin-ai-integration[bot] Nov 12, 2026
f07563d
test(repl): keep the open-bound test's comment to two lines
devin-ai-integration[bot] Nov 12, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions changes/unreleased/smt-divergence-pair-order.fixed.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
- A sensitivity divergence found by the SMT engine (`%check-diverge`) spells its two final values in the check engine's order, `x ends as 1 or 2`, whichever copy the solver gave which value; z3 4.13 answers the copies the other way round from 4.8, and the report, the witness pair and the REPL's test depended on it. The optimizer's open-bound test likewise accepts either a named bound (z3 4.13: approached without being attained) or an unestablished optimum (z3 4.8), never a value standing for the optimum.
6 changes: 6 additions & 0 deletions internal/exec/smt/twocopy.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -198,6 +198,12 @@ func (e *Encoding) DecodePair(result *solve.Result, out Output) (*Diverging, err
if d.Values[0] == d.Values[1] {
return nil, &WitnessError{Var: out.Var.Name, Reason: fmt.Sprintf("both copies end with %s", d.Values[0])}
}
// The check engine spells a divergence's values in string order; which copy the solver
// gave which value is its own choice (z3 4.8 and 4.13 differ), so the pair is ordered here.
if d.Values[0] > d.Values[1] {
d.Runs[0], d.Runs[1] = d.Runs[1], d.Runs[0]
d.Values[0], d.Values[1] = d.Values[1], d.Values[0]
}
return d, nil
}

Expand Down
11 changes: 7 additions & 4 deletions internal/frontend/repl/optimize_test.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -221,8 +221,8 @@ func TestOptimizeReportsObjectivesInDeclarationOrder(t *testing.T) {
}
}

// A bound no assignment attains is never reported as a value: the report says
// there is no optimum and offers only the feasible value found.
// A bound no assignment attains is never reported as a value: the report says there is no optimum,
// or (z3 4.13 names the bound, 4.8 does not) that it is approached without being attained.
func TestOptimizeReportsABoundThatIsNotAttained(t *testing.T) {
requireOptimizingSolver(t)
s := checkSession(t, optimizeModel)
Expand All @@ -231,8 +231,11 @@ func TestOptimizeReportsABoundThatIsNotAttained(t *testing.T) {
t.Fatalf("status is %s, want no-optimum: %s", report.Status, strings.Join(report.Lines, "\n"))
}
wants(t, got, "! Analysis OpenBound is satisfiable, but its optimum was not established",
"maximize widest = `margin`: no optimum reported")
rejects(t, got, "is optimized")
"maximize widest = `margin`: no ")
if !strings.Contains(got, "no optimum reported") && !strings.Contains(got, "no greatest value, approaching 10.5 without attaining it") {
t.Errorf("the open bound is neither reported as unestablished nor as approached without being attained:\n%s", got)
}
rejects(t, got, "is optimized", "widest = `margin`: 10.5")
}

// Refusals need no solver: they are settled while translating.
Expand Down
Loading