diff --git a/changes/unreleased/codegen-rec-parse-declaration.fixed.md b/changes/unreleased/codegen-rec-parse-declaration.fixed.md
new file mode 100644
index 0000000000..72edf108af
--- /dev/null
+++ b/changes/unreleased/codegen-rec-parse-declaration.fixed.md
@@ -0,0 +1 @@
+- The generated C of a function whose program holds records declares `sysml_parse_rec`, so the collection runtime it instantiates over records compiles under a C compiler that rejects implicit declarations (gcc 14 and later); the compiler is now asked to reject them everywhere (`-Werror=implicit-function-declaration`).
diff --git a/changes/unreleased/smt-sensitivity-value-order.fixed.md b/changes/unreleased/smt-sensitivity-value-order.fixed.md
new file mode 100644
index 0000000000..28de97c607
--- /dev/null
+++ b/changes/unreleased/smt-sensitivity-value-order.fixed.md
@@ -0,0 +1 @@
+- A sensitivity the SMT engine witnesses spells the output's two values in the check engine's order (`x ends as 1 or 2`), with witness A the run that ends with the first, whichever copy the solver's model put first.
diff --git a/docs/project/native-compilation.md b/docs/project/native-compilation.md
index 076b92f13f..80571a5879 100644
--- a/docs/project/native-compilation.md
+++ b/docs/project/native-compilation.md
@@ -407,7 +407,7 @@ lower.CalcBody (statements) ──┘
   checked-arithmetic prelude, the calcs as functions, a `sysml_run` entry that turns an error into
   a status, and a `main`.
 - `build.go` — `Source`, `Build`, `Targets`; C is compiled with
-  `-O3 -flto -std=gnu11 -Wall -Wextra`, Go in a throwaway module.
+  `-O3 -flto -std=gnu11 -Werror=implicit-function-declaration -Wall -Wextra`, Go in a throwaway module.
 
 ### Function values
 
diff --git a/internal/exec/smt/twocopy.go b/internal/exec/smt/twocopy.go
index d1ea0e72dd..22d956b115 100644
--- a/internal/exec/smt/twocopy.go
+++ b/internal/exec/smt/twocopy.go
@@ -198,6 +198,11 @@ 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 orders a divergence's values; which copy the solver put first is noise.
+	if d.Values[1] < d.Values[0] {
+		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..4b4d09f2bb 100644
--- a/internal/frontend/repl/optimize_test.go
+++ b/internal/frontend/repl/optimize_test.go
@@ -222,7 +222,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.
+// there is no optimum and offers only the feasible value found. Whether the
+// solver names the bound it approaches (z3 4.13) or reports nothing (z3 4.8)
+// depends on its version; what it must never do is report the bound as a value.
 func TestOptimizeReportsABoundThatIsNotAttained(t *testing.T) {
 	requireOptimizingSolver(t)
 	s := checkSession(t, optimizeModel)
@@ -231,8 +233,12 @@ 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, "`margin`: no optimum reported") &&
+		!strings.Contains(got, "`margin`: no greatest value, approaching 10.5 without attaining it") {
+		t.Errorf("the open bound is neither unreported nor reported as approached:\n%s", got)
+	}
+	rejects(t, got, "is optimized", "`margin`: 10.5")
 }
 
 // Refusals need no solver: they are settled while translating.
diff --git a/internal/translate/codegen/build.go b/internal/translate/codegen/build.go
index 603547ccaa..17e1d7c28d 100644
--- a/internal/translate/codegen/build.go
+++ b/internal/translate/codegen/build.go
@@ -52,7 +52,7 @@ func goCommand(name string) (string, error) {
 
 // CFlags are the C compiler options; the prelude's explicit checks keep -O3 safe,
 // and no contraction keeps every Real operation rounded as the interpreter rounds it.
-var CFlags = []string{"-O3", "-flto", "-ffp-contract=off", "-std=gnu11", "-Wall", "-Wextra", "-Wno-unused-function", "-Wno-unused-parameter"}
+var CFlags = []string{"-O3", "-flto", "-ffp-contract=off", "-std=gnu11", "-Werror=implicit-function-declaration", "-Wall", "-Wextra", "-Wno-unused-function", "-Wno-unused-parameter"}
 
 // Source renders program for target, as a complete program with a main.
 func Source(p *Program, target Target) ([]byte, error) {
diff --git a/internal/translate/codegen/emit_fn.go b/internal/translate/codegen/emit_fn.go
index 33488d072f..1674294020 100644
--- a/internal/translate/codegen/emit_fn.go
+++ b/internal/translate/codegen/emit_fn.go
@@ -304,6 +304,7 @@ static const char *sysml_show_rec(sysml_rec *r) {
 	sysml_format_rec(r, text, sizeof text);
 	return text;
 }
+static sysml_rec *sysml_parse_rec(const char *s, const char *name) { fprintf(stderr, "argument %s: %s is not an object value\n", name, s); exit(2); }
 ` + r.Replace(cSeqTemplate)
 }