Pin HiGHS_jll below 1.15 and assert solve status in tests (#220)

## Why this matters

MIPVerify's repository jobs became unreliable after the Julia workspace
began resolving HiGHS.jl 1.24.1 with HiGHS_jll 1.15.1. Issues #218 and
#219 record native solver crashes on Ubuntu, Windows, and macOS, plus
repeated unexpected objective values for the same macOS test.

A [standalone reproducer for that test
workload](#219 (comment))
crashed in 3 of 5 process runs with 1.15.1. The observed crashes
occurred with `threads = 1` and `parallel = "off"`, so those settings
did not prevent the reproduced failure. The same script completed 3 of 3
runs with 1.14.0, and every full solve finished `OPTIMAL` at the
expected objective. These small samples support temporarily excluding
1.15.x from this repository; they do not estimate a stable failure rate.

The objective-mismatch CI logs did not record termination status. They
therefore cannot show whether HiGHS claimed optimality at the unexpected
value or stopped early with a feasible incumbent. A separately checked
feasible point at 6.959316 proves that the reported 9.323265 value
cannot be the optimum, but it does not recover the missing status.

[HiGHS 1.15.0](https://github.com/ERGO-Code/HiGHS/releases/tag/v1.15.0)
was the first release of its parallel mixed-integer programming (MIP)
solver. A relevant upstream fix,
[ERGO-Code/HiGHS#3141](ERGO-Code/HiGHS#3141),
removes non-thread-safe C API scheduler resets that can cause random
Julia-test segfaults. It merged after HiGHS 1.15.1; no released HiGHS
version contained the fix as of July 16, 2026. The exact MIPVerify
reproducer has not been tested against that fix, so the pin should
remain until a released binary includes it and this workload passes
local and CI validation.

## What changes

- Add `HiGHS_jll = "~1.14"` to the test project's dependencies and
compatibility bounds. Because the repository uses a Julia workspace,
this constrains tests, benchmarks, and examples. Current registry
metadata resolves HiGHS.jl 1.23.0 with HiGHS_jll 1.14.0. MIPVerify's
package dependencies are unchanged; downstream users can resolve other
HiGHS versions.
- For adversarial-example tests with a finite expected objective, record
a separate `SolveStatus == OPTIMAL` assertion before the existing
objective comparison. A future log will show whether a mismatch followed
an optimal or non-optimal termination. The existing objective checks
continue after the assertion; infeasible cases are unchanged.

Mitigates #218 and #219.

## Validation

- `julia --project=. -e 'using Pkg; Pkg.test(; coverage=false)'` on a
local merge of `047f47e` into `105b11e`: 613 passed, 1 expected broken,
614 total. The resolved solver pair was HiGHS.jl 1.23.0 with HiGHS_jll
1.14.0.
- [GitHub Actions run
29528616336](https://github.com/vtjeng/MIPVerify.jl/actions/runs/29528616336):
all 15 checks passed for head `047f47e`, including all six OS/version
package-test jobs. That run used base `8a455e2`; the local merge test
above covers the later base.
- `git diff --check` passes.

For the [solver-version
comparison](#219 (comment)),
three matched full-suite runs used Linux x64, Julia 1.12.6, and the same
521-test selection:

| Run | 1.15.1 baseline | Pinned 1.14.0 | Pinned / baseline |
| --- | ---: | ---: | ---: |
| 1 | 260.7 s | 263.6 s | 1.01× |
| 2 | 279.1 s | 260.0 s | 0.93× |
| 3 | 266.0 s | 250.8 s | 0.94× |
| **Total** | **805.8 s** | **774.4 s** | **0.96× (3.9% lower)** |

The aggregate wall time was 3.9% lower with the pin. One machine and
three pairs are insufficient to characterize general solver performance
or the failure rate.

Author: vtjeng

test/Project.toml

@@ -2,6 +2,7 @@
 CSV = "336ed68f-0bac-5ca0-87d4-7b16caf5d00b"
 DataFrames = "a93c6f00-e57d-5684-b7b6-d8193f3e46c0"
 HiGHS = "87dc4568-4c63-4d18-b0c0-bb2238e4078b"
+HiGHS_jll = "8fd58aa0-07eb-5a78-9b36-339c94fd15ea"
 IntervalArithmetic = "d1acc4aa-44c8-5952-acd4-ba5d80a2a253"
 JuMP = "4076af6c-e467-56ae-b986-b466b2749572"
 MIPVerify = "e5e5f8be-2a6a-5994-adbb-5afbd0e30425"
@@ -15,4 +16,8 @@ MIPVerify = {path = ".."}
 
 [compat]
 HiGHS = "1.4"
+# HiGHS 1.15.x introduced a parallel MIP solver that segfaults and returns
+# nondeterministic results, even with threads=1 (issue #219); unpin once
+# upstream stabilizes.
+HiGHS_jll = "~1.14"
 TimerOutputs = "0.5"

test/TestHelpers.jl

@@ -81,6 +81,9 @@ function test_find_adversarial_example(
         @test d[:SolveStatus] == MathOptInterface.INFEASIBLE ||
               d[:SolveStatus] == MathOptInterface.INFEASIBLE_OR_UNBOUNDED
     else
+        # Distinguishes solver wrong answers (OPTIMAL at a bad objective) from early
+        # termination with a feasible incumbent; see issue #219.
+        @test d[:SolveStatus] == MathOptInterface.OPTIMAL
         actual_objective_value = JuMP.objective_value(d[:Model])
         if expected_objective_value == 0
             @test isapprox(actual_objective_value, expected_objective_value; atol = 1e-4)