From c41ec8096bce246d4fff373bae2380a706623b4d Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Thu, 12 Nov 2026 05:30:34 +0000 Subject: [PATCH 1/2] fix(smt): spell a divergence's values in the check engine's order whichever copy the solver gave which z3 4.13 answers the two-copy sensitivity query with the copies the other way round from 4.8, so the report, the witness pair and the test depended on the solver; the pair is now ordered as runtime's Divergence is. The optimizer's open-bound test asserts the semantics (no optimum, no value standing for it) and accepts either a named bound or an unestablished optimum. Co-Authored-By: jason.han --- .../unreleased/smt-divergence-pair-order.fixed.md | 1 + internal/exec/smt/twocopy.go | 6 ++++++ internal/frontend/repl/optimize_test.go | 12 ++++++++---- 3 files changed, 15 insertions(+), 4 deletions(-) create mode 100644 changes/unreleased/smt-divergence-pair-order.fixed.md diff --git a/changes/unreleased/smt-divergence-pair-order.fixed.md b/changes/unreleased/smt-divergence-pair-order.fixed.md new file mode 100644 index 0000000000..7301f34b71 --- /dev/null +++ b/changes/unreleased/smt-divergence-pair-order.fixed.md @@ -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. diff --git a/internal/exec/smt/twocopy.go b/internal/exec/smt/twocopy.go index d1ea0e72dd..656eefa228 100644 --- a/internal/exec/smt/twocopy.go +++ b/internal/exec/smt/twocopy.go @@ -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 } diff --git a/internal/frontend/repl/optimize_test.go b/internal/frontend/repl/optimize_test.go index 5a07659106..8fc946790b 100644 --- a/internal/frontend/repl/optimize_test.go +++ b/internal/frontend/repl/optimize_test.go @@ -221,8 +221,9 @@ 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 and, when the solver names the bound (z3 4.13 does, 4.8 does not), that it is approached +// without being attained; either way only the feasible value found is offered. func TestOptimizeReportsABoundThatIsNotAttained(t *testing.T) { requireOptimizingSolver(t) s := checkSession(t, optimizeModel) @@ -231,8 +232,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. From f07563d2304175eeecbb12d6ae5c089d02578fed Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Thu, 12 Nov 2026 05:43:23 +0000 Subject: [PATCH 2/2] test(repl): keep the open-bound test's comment to two lines Co-Authored-By: jason.han --- internal/frontend/repl/optimize_test.go | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/internal/frontend/repl/optimize_test.go b/internal/frontend/repl/optimize_test.go index 8fc946790b..73aace55fd 100644 --- a/internal/frontend/repl/optimize_test.go +++ b/internal/frontend/repl/optimize_test.go @@ -221,9 +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, when the solver names the bound (z3 4.13 does, 4.8 does not), that it is approached -// without being attained; either way only the feasible value found is offered. +// 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)