## Problem
Maximizing/minimizing under a **strict** inequality has a delta-rational
optimum. For
```smt2
(declare-const r Real)
(assert (< r 1))
(maximize r)
(check-sat)
(get-objectives)
```
the optimum is the supremum `1 - epsilon`, but z3 reported `r = 0`.
The same defect makes shared-symbol objectives report a value matching
**neither the model nor the true optimum** (issue #10028 follow-up).
Minimal reproducer — a 6-mark Golomb ruler (a `>32`-arg `distinct`, so
the objective is coupled to EUF) with a strict real objective `obj >
x5`, whose true optimum is `17 + epsilon`:
| case | before | after |
|---|---|---|
| `maximize r`, `r < 1` | `0` ❌ | `1 - epsilon` ✅ |
| `minimize r`, `r > 1` | `0` ❌ | `1 + epsilon` ✅ |
| Golomb `minimize obj`, `obj > x5` | `35/2` / `7+eps` ❌ | `17 +
epsilon` ✅ |
## Root cause
`check_bound` validates the LP hint by asserting `objective >= optimum`.
For a supremum `1 - epsilon` this is a **lower** bound whose value
carries a **negative** infinitesimal `(1, -1)`.
No `lconstraint_kind` can express that. The kind->infinitesimal map only
yields the *matching-sign* cases — `GT` -> lower `(r, +1)`, `LT` ->
upper `(r, -1)` — or zero (`GE`/`LE`). The opposite-sign lower bound
`(r, -1)` (i.e. `r >= r0 - delta`) is a *relaxation* that no strict
inequality produces. `opt_solver::mk_ge` therefore projected the
`-epsilon` away, turning `r >= 1 - epsilon` into the over-strong,
unsatisfiable `r >= 1`; validation failed and the strictly smaller
current model value was reported instead.
## Fix — carry the infinitesimal faithfully through the bound pipeline
- **`lp_api::bound`** gains an `eps` component so `get_value` returns
the true delta value (no spurious rational fixed-variable equality is
propagated to EUF).
- **`lar_base_constraint`** stores its right-hand side as a
delta-rational `impq` pair; `rhs()` returns the rational component,
`bound_eps()` the infinitesimal one.
- **`lar_solver`** bound activation/update threads the whole `impq`
bound, so a lower bound `(r, -1)` can be asserted. `constraint_holds`
accounts for it using the **same** strict-bounds delta that flattens the
model, computed **once per model**.
- **`theory_lra::mk_ge`** builds a *fresh* predicate for the `(r, -1)`
lower bound (to avoid colliding with an already-internalized `v >= r`
literal) and attaches `eps = -1`. **`opt_solver::mk_ge`** passes the
unprojected value to `theory_lra` / `theory_mi_arith` /
`theory_inf_arith` (whose bounds are already `inf_rational`).
The pair machinery is what makes the supremum both representable
(optimum `1 - epsilon`) and validatable; the reported witness model
remains the flattened rational (`find_delta_for_strict_bounds`),
consistent with the existing epsilon semantics.
## Validation
- Strict optima correct: `1-eps`, `1+eps`, bounded `2<r<5 -> 5-eps`, and
lex/box variants.
- Integer optima and the #10028 shared-symbol cases unchanged (Golomb
n=6/7/8 -> 17/25/34, consistent with the model).
- Unit tests **92/92** (release); no new debug-suite failures.
- Opt regression corpus (73 files, `model_validate=true`)
**byte-identical** to baseline.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
[//]: # (dependabot-start)
⚠️ **Dependabot is rebasing this PR** ⚠️
Rebasing might not happen immediately, so don't worry if this takes some
time.
Note: if you make any changes to this PR yourself, they will take
precedence over the rebase.
---
[//]: # (dependabot-end)
Bumps [actions/cache](https://github.com/actions/cache) from 6.0.0 to
6.1.0.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/releases">actions/cache's
releases</a>.</em></p>
<blockquote>
<h2>v6.1.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Bump <code>@actions/cache</code> to v6.1.0 - handle read-only cache
access by <a
href="https://github.com/jasongin"><code>@jasongin</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1768">actions/cache#1768</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v6...v6.1.0">https://github.com/actions/cache/compare/v6...v6.1.0</a></p>
</blockquote>
</details>
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/blob/main/RELEASES.md">actions/cache's
changelog</a>.</em></p>
<blockquote>
<h3>6.1.0</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v6.1.0 to pick up <a
href="https://redirect.github.com/actions/toolkit/pull/2435">actions/toolkit#2435
Handle cache write error due to read-only token</a></li>
<li>Switch redundant "Cache save failed" warning to debug log
in save-only</li>
</ul>
</blockquote>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="55cc834586"><code>55cc834</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/cache/issues/1768">#1768</a>
from jasongin/readonly-cache</li>
<li><a
href="d8cd72f230"><code>d8cd72f</code></a>
Bump <code>@actions/cache</code> to v6.1.0 - handle cache write error
due to RO token</li>
<li>See full diff in <a
href="https://github.com/actions/cache/compare/v6.0.0...v6.1.0">compare
view</a></li>
</ul>
</details>
<br />
[](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores)
Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
<details>
<summary>Dependabot commands and options</summary>
<br />
You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)
</details>
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Bumps [actions/cache](https://github.com/actions/cache) from 5.0.5 to
6.0.0.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/releases">actions/cache's
releases</a>.</em></p>
<blockquote>
<h2>v6.0.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Update packages, migrate to ESM by <a
href="https://github.com/Samirat"><code>@Samirat</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1760">actions/cache#1760</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v5...v6.0.0">https://github.com/actions/cache/compare/v5...v6.0.0</a></p>
</blockquote>
</details>
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/blob/main/RELEASES.md">actions/cache's
changelog</a>.</em></p>
<blockquote>
<h3>6.0.0</h3>
<ul>
<li>Updated <code>@actions/cache</code> to ^6.0.1,
<code>@actions/core</code> to ^3.0.1, <code>@actions/exec</code> to
^3.0.0, <code>@actions/io</code> to ^3.0.2</li>
<li>Migrated to ESM module system</li>
<li>Upgraded Jest to v30 and test infrastructure to be ESM
compatible</li>
</ul>
<h3>5.0.4</h3>
<ul>
<li>Bump <code>minimatch</code> to v3.1.5 (fixes ReDoS via globstar
patterns)</li>
<li>Bump <code>undici</code> to v6.24.1 (WebSocket decompression bomb
protection, header validation fixes)</li>
<li>Bump <code>fast-xml-parser</code> to v5.5.6</li>
</ul>
<h3>5.0.3</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v5.0.5 (Resolves: <a
href="https://github.com/actions/cache/security/dependabot/33">https://github.com/actions/cache/security/dependabot/33</a>)</li>
<li>Bump <code>@actions/core</code> to v2.0.3</li>
</ul>
<h3>5.0.2</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v5.0.3 <a
href="https://redirect.github.com/actions/cache/pull/1692">#1692</a></li>
</ul>
<h3>5.0.1</h3>
<ul>
<li>Update <code>@azure/storage-blob</code> to <code>^12.29.1</code> via
<code>@actions/cache@5.0.1</code> <a
href="https://redirect.github.com/actions/cache/pull/1685">#1685</a></li>
</ul>
<h3>5.0.0</h3>
<blockquote>
<p>[!IMPORTANT]
<code>actions/cache@v5</code> runs on the Node.js 24 runtime and
requires a minimum Actions Runner version of <code>2.327.1</code>.
If you are using self-hosted runners, ensure they are updated before
upgrading.</p>
</blockquote>
<h3>4.3.0</h3>
<ul>
<li>Bump <code>@actions/cache</code> to <a
href="https://redirect.github.com/actions/toolkit/pull/2132">v4.1.0</a></li>
</ul>
<h3>4.2.4</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v4.0.5</li>
</ul>
<h3>4.2.3</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v4.0.3 (obfuscates SAS token in
debug logs for cache entries)</li>
</ul>
<h3>4.2.2</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v4.0.2</li>
</ul>
<h3>4.2.1</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v4.0.1</li>
</ul>
<!-- raw HTML omitted -->
</blockquote>
<p>... (truncated)</p>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="2c8a9bd745"><code>2c8a9bd</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/cache/issues/1760">#1760</a>
from actions/samirat/esm_migration_and_package_update</li>
<li><a
href="e9b91fdc3f"><code>e9b91fd</code></a>
Prettier fixes</li>
<li><a
href="e4884b8ff7"><code>e4884b8</code></a>
Rebuild dist</li>
<li><a
href="10baf0191a"><code>10baf01</code></a>
Fixed licenses</li>
<li><a
href="e39b386c90"><code>e39b386</code></a>
Fix test mock return order</li>
<li><a
href="b692820337"><code>b692820</code></a>
PR feedback</li>
<li><a
href="60749128a4"><code>6074912</code></a>
Rebuild dist bundles as ESM to match type:module</li>
<li><a
href="5a912e8b4a"><code>5a912e8</code></a>
Fix lint and jest issues</li>
<li><a
href="b9bf592b98"><code>b9bf592</code></a>
Update documentation for v6 release</li>
<li><a
href="80f777761d"><code>80f7777</code></a>
Update packages, migrate to ESM</li>
<li>See full diff in <a
href="https://github.com/actions/cache/compare/v5.0.5...v6.0.0">compare
view</a></li>
</ul>
</details>
<br />
[](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores)
Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
<details>
<summary>Dependabot commands and options</summary>
<br />
You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)
</details>
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
* fix: add generating META for ocamlfind.
* Patch macos. We need to keep the `@rpath` and use environment var to enable the test because we need to leave it to be fixed by package managers.
* Trigger CI.
* Debug.
* Debug.
* Debug.
* Debug.
* Debug.
* Debug.
* Hacky fix for ocaml building warning.
* Fix typo and rename variables.
* Update doc for `mk_context`.
* Migrating to cmake.
* Migrating to cmake. It builds both internal or external libz3.
* Start to work on platform-specific problem.
* Messy notes.
* debug.
* Cleanup a bit.
* Fixing shared lib extension.
* Minor.
* Resume working on this PR.
* Remove including `AddOCaml`.
* Keep `z3.ml` and `z3.mli` in the src but specify the generated file in the bin.
* Keep `ml_example.ml` in the src.
* Try github action for ocaml.
* Add workflow using matrix.
* Fix mac linking once more.
* Bypass @rpath in building sanity check.
