[ondrik]

Targets devel (rebased on 28 Oct).

These build failures were found by the platform probe in draft #46. Each one breaks a configuration that tests.yml (GCC 13 on Ubuntu 24.04) can't see.

1. GMP leaf type on GCC 14+ and clang: now on devel

This PR originally added <stdio.h> before every <gmp.h>. devel has since fixed the same failure in the two headers that need it (3755811), so that part was dropped from this PR in the rebase.

2. No release build on macOS

Apple clang rejects -ffat-lto-objects, which every release build passed, so nothing built on a Mac without LTO=0.

The Makefile now adds the flag only where the compiler accepts it, checked once per make run. The check passes -flto too, because Apple clang accepts -ffat-lto-objects on its own and rejects it only together with -flto. GCC and clang 18 still get the flag.

3. f128 without libquadmath

Under clang (Linux or macOS), and on arm64 macOS in general, building f128 failed on a bare 'quadmath.h' file not found. It now stops with:

LEAF_FLOAT_TYPE=3 (__float128, the default) needs GCC's libquadmath, which this compiler lacks; build another leaf type, e.g. make buddy_doubles_f64

f128 stays the default leaf type, so nothing changes where it builds today.

4. GMP builds linked libquadmath

-lquadmath was added to every link whenever the default leaf type is f128, GMP builds included. macOS has no libquadmath, so buddy_gmp failed to link there.

The GMP links now use CLIBS_GMP, which leaves libquadmath out. Verified locally: the GMP binary no longer depends on libquadmath, and test_unit_leaf_gmp passes.

Result

In #46, every leaf type now builds and passes on all of the following, except f128 under clang, which stops with the error above:

• Ubuntu 22.04 (GCC 11), 24.04 (GCC 13) and 26.04 (GCC 15);
• Ubuntu 24.04 with clang 18;
• macOS on Apple Silicon.

Not included

• flex/bison: MoToBuddy needed them for its bddcalc example. This is fixed upstream in VeriFIT/MoToBuddy@acc4c26, and MEDUSA picks it up with the pin bump in build: bump MoToBuddy to acc4c26 (no flex/bison needed) #50.
• GCC 9: it can't compile MoToBuddy's declarations after case labels. That's still the case at acc4c26, so GCC 11 (Ubuntu 22.04) remains the minimum.

Both belong upstream in MoToBuddy or in the README. Ubuntu 20.04 is dropped from #46.

#46 is stacked on this branch, so its matrix checks these fixes across the platforms.

🤖 Generated with Claude Code

https://claude.ai/code/session_012q87VyzNBV8gtH2ntMeKoM

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

[github-actions]

Claude Code review (CERIT, model coder) of bc090c2

I read claude-review-input/pr.md and claude-review-input/pr.diff (the diff ends cleanly — it shows the two changed files in full, no "files not shown" note), then checked the surrounding sources (Makefile, the leaf headers, src/mtbdd_out.*, the include order of every <gmp.h> user, and the CI workflows' make invocations).

Findings:

• claude-review-input/pr.md §1 vs. the diff - the PR's headline fix Add MoToBuddy floating-point backend #1 ("every header that includes <gmp.h> now includes <stdio.h> first") is not present in this diff. The diff touches only Makefile and src/interface_implementations/leaf_primitives/leaf_primitive_double.h, and neither adds a <stdio.h> before a <gmp.h>. The checked-out tree does contain that fix in src/mtbdd_out.h:11-16 and src/interface_implementations/leaf_primitives/leaf_primitive_mpz.h:7-13, so it may already be on the base branch this PR is stacked on — I can't run git here to confirm. But if it is not, then this PR does not deliver item 1 as described: src/hash.h:7, src/htab.c:3, src/symexp_list.h:7, src/mtbdd.h:6, src/interface_implementations/inc/interface_leaf.h:10, interface_bdd_core.h:5 and interface_norm.h:5 all still include <gmp.h> with no preceding <stdio.h>. They are only safe because every build rule force-includes a leaf header (which pulls in <stdio.h>) ahead of the source file; any new compile rule that forgets the -include reintroduces the __gmpz_out_str implicit-declaration error on GCC 14/clang 16+. The author should confirm the stdio.h-before-gmp.h changes are actually in a merged commit of this stack, or add them to this PR.

• Makefile:126-129 - the -ffat-lto-objects probe treats any failure of the test compile as "flag unsupported", with all diagnostics discarded (2>/dev/null) and no fallback warning. Scenario: a sandboxed/locked-down environment where $(CC) cannot exec the LTO plugin or write a temp file at make parse time (or where /dev/null is unusable) makes the probe exit non-zero for reasons unrelated to the flag, so a GCC release build silently loses fat LTO objects; the build and make LTO=1 links still succeed, but the documented make LTO=0 relink-without-rebuild (Makefile:26-27) then fails on LTO-only objects with no hint why. A one-line $(warning ...) when the probe unexpectedly fails on a GCC-family compiler would make this diagnosable. Minor, and it does not affect any configuration the current CI runs (all ubuntu-latest + gcc, where the probe passes and behaviour is unchanged from before the PR).

I could not find any correctness, refcount/GC, leak, or numerical-behaviour issue in the changed code itself: the CLIBS_GMP filter-out is applied to every GMP link line in the Makefile (I checked sylvan_gmp, test_unit_leaf_gmp, test_grover_gmp, test_grover_sylvan_gmp, test_stress_gmp, buddy_gmp — none is missed), it is defined after the final -lstdc++ append so it sees the complete CLIBS, and the __has_include guard in leaf_primitive_double.h:87-89 only replaces a bare 'quadmath.h' file not found with a clearer error on every platform I could construct (GCC/clang Linux with libquadmath-dev, Apple clang, arm64), leaving working configurations building exactly as before. CI (tests.yml, nightly.yml, coverage.yml) is ubuntu+gcc only, so the probe and the new #error are no-ops there.
_{Automated and advisory: it may be wrong, and it does not block merging. Run.}