Add a build script for Yices on macOS

[daniel-raffler]

Hello,

this PR adds an ant target for building the Yices library on macOS. We can't currently ship the binary due to a lack of Apple hardware and the signing issue. However, the script allows users to at least build the binaries themselves

I've tested this on my JavaSMT fork with a github runner and was able to build the binaries and then run the tests

@kfriedberger
We could also include some of the changes I made to the CI on my fork. Building the Yices binaries separately adds 5-10 minutes to each test run, so we should probably limit it to just one Java version on macOS

Do you think it's worth the extra trouble?

[ThomasHaas]

I tried to build script and while it worked fine, I still couldn't get Yices2 to run via JavaSMT.

First, I got a class load error for Yices2SolverContext, but that was because I needed to update our pom.xml.
Then I added the binary to our standard location for solver libraries.
I got this error

The SMT solver YICES2 is not available on this machine because of missing libraries 
(no yices2j in java.library.path: [...])

Notice how the library name yices2j JavaSMT (v5.0.1) looks for does not match with the library name libyices2java.dylib the build script generates. Thinking it was just a name mismatch, I renamed the binary to yices2j.dylib but that didn't resolve the problem.

Any ideas about what could have gone wrong? Maybe it just doesn't work with the JavaSMT v5.0.1? The newest version is not yet available on maven.

[daniel-raffler]

Hello Thomas,

thanks for giving it a try!

Any ideas about what could have gone wrong? Maybe it just doesn't work with the JavaSMT v5.0.1? The newest version is not yet available on maven.

Yes, this will require the upcoming JavaSMT 6.1 release. We recently made some changes to the Yices backend, so the binary won't work with older versions

If you're interested, you should be able to check that the binary is working like this:

ant build
java -cp bin:lib/java/core/*:lib/java/runtime-yices2/* org.sosy_lab.java_smt.example.SolverOverviewTable

or by simply running the tests:

ant unit-tests-quick

[ThomasHaas]

java -cp "bin:lib/java/core/*:lib/java/runtime-yices2/*" org.sosy_lab.java_smt.example.SolverOverviewTable
+-----------------------+------------------------------------------+------------------------------------------+------------------------------------------+
| YICES2                | Yices 2.7.0                              | Integer, Bitvector, Rational, Array,     | Interpolation, Assumptions, UnsatCore /w |
|                       |                                          | Quantifier, UF                           | Assumption, UnsatCore                    |
+-----------------------+------------------------------------------+------------------------------------------+------------------------------------------+

Looks good I guess :)

[kfriedberger]

Hi together, let me join the conversation here.

Maven

Our Maven deployment has been non-functional since July 2025 (see #385) ❌. While @ThomasHaas is the first to officially mention this, we recognize that our visibility into the user base is limited, and we've historically prioritized issues based on community feedback, aka "who cries loudest" 😄. Although we aimed (and missed) to resolve this with the JavaSMT 6.0.0 release last month, a working solution is still not available. 😢

Roadmap for Resolution: 📶 (see also #385)

• Modernize Deployment Scripts: Replace the outdated 2014 Ant/Ivy scripts with a new publication process. This removes the need for a separate, manual build of JavaSMT just for Maven.
• Ivy-to-Maven Synchronization: Implement a "copy-over" mechanism for releases, as it has already been used for solver binaries. This will allow us to back-fill all versions of JavaSMT missed since July 2025 and simplify future releases.

macOS

Providing macOS-specific binary libraries depends entirely on our ability to implement a viable certification and signing process. This presents two primary challenges:

• Integration with Linux-based CI: Our release pipeline is standardized on a Linux-based Docker environment. Neither JavaSMT nor Sosy-Lab currently has the resources to maintain separate release infrastructures for different operating systems. We already manage enough complexity with our various solver-specific build steps. 😄 In the meantime, we provide guidance (like this PR) to help users compile binaries on their own systems.
• Certification: While we could potentially distribute self-signed binaries via our standard release cycle, execution remains a major hurdle. 🗝️ Per Apple’s security policy, unsigned or self-signed binaries are often restricted to the system that built them, making them difficult for end-users to run. 🍎 ⛔ We are exploring whether GitHub Runners can be used for testing, provided we find a reliable way to authorize self-signed libraries. These same workarounds might work for technically-inclined users, but they aren't a seamless experience. As a last resort, we could register a Apple Developer account with a yearly fee. There might be discounted options available for open-source or educational projects. 💸

I have a few upcoming free days, where I will look into those topics. ✅

[ThomasHaas]

Providing macOS-specific binary libraries depends entirely on our ability to implement a viable certification and signing process.

I don't think it has such a high priority. This PR at least allows for tool developers that rely on JavaSMT to try out more solvers, even if users of said tool are not yet able to due to missing binaries (they surely won't want to build the binaries on their systems).
I think getting maven deployment to work again is a lot more important :)