Add CI for example projects by daniel-raffler · Pull Request #667 · sosy-lab/java-smt

daniel-raffler · 2026-05-30T11:32:03Z

Hello everyone,

this PR adds CI checks for all project examples in the doc directory to verify that they're working, and make sure that there are no issues with the packages that we've published to Maven. It is based on two earlier PRs that update the example projects and add another project template for using JavaSMT in Ivy. As a result, this PR now contains CI for using JavaSMT with 5 different build systems:

Maven
Maven Web
Gradle
Kotlin/Gradle
Ivy

Except for Maven Web, all CI checks are run multiple times to cover all supported platforms. For Maven Web the project is a web application and we only test x64-linux as this is most likely what the server will use. Also note, that for the web application we don't actually test if the *.war is working as this would be too difficult to do inside of a Github workflow

Results from the latest CI run can be found here for my fork of the project. To make it work here we would still have to whilelist an action that is used by the workflow, see here

Closes #663

…ion number to the example project

… the starter guide

…o the starter guide

… the other template projects

…oblems-with-installation

daniel-raffler · 2026-06-01T18:43:48Z

+        private val OS: String =
+            StandardSystemProperty.OS_NAME.value()!!.lowercase(Locale.getDefault()).replace(" ", "")
+        private val ARCH: String =
+            StandardSystemProperty.OS_ARCH.value()!!.lowercase(Locale.getDefault()).replace(" ", "")
+
+        protected val IS_WINDOWS: Boolean = OS.startsWith("windows")
+        private val IS_MAC: Boolean = OS.startsWith("macos")
+        private val IS_LINUX: Boolean = OS.startsWith("linux")
+
+        private val IS_ARCH_ARM64 = ARCH == "aarch64"
+
+        private fun isSufficientVersionOfLibcxx(library: String): Boolean {
+            try {
+                NativeLibraries.loadLibrary(library)
+            } catch (e: UnsatisfiedLinkError) {
+                for (dependency in getRequiredLibcxx(library)) {
+                    if (e.message!!.contains("version `" + dependency + "' not found")) {
+                        return false
+                    }
+                }
+            }
+            return true
+        }
+
+        private fun getRequiredLibcxx(library: String): List<String> {
+            return when (library) {
+                "z3" -> listOf("GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29")
+                "bitwuzlaj" -> listOf("GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29")
+                "opensmtj" -> listOf("GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29")
+                "mathsat5j" -> listOf("GLIBC_2.33", "GLIBC_2.38")
+                "cvc5jni" -> listOf("GLIBC_2.32")
+                "yices2java" -> listOf("GLIBC_2.34")
+                else -> listOf()
+            }
+        }
+
+        /** Disable some checks on certain combinations of operating systems and solvers, because of missing dependencies.  */
+        private fun isSupportedOperatingSystemAndArchitecture(solver: Solvers): Boolean {
+            return when (solver) {
+                Solvers.SMTINTERPOL, Solvers.PRINCESS -> true
+                Solvers.BOOLECTOR, Solvers.CVC4 -> IS_LINUX && !IS_ARCH_ARM64
+                Solvers.YICES2 -> (IS_LINUX && !IS_ARCH_ARM64 && isSufficientVersionOfLibcxx("yices2java"))
+                        || (IS_WINDOWS && !IS_ARCH_ARM64)
+
+                Solvers.CVC5 -> (IS_LINUX && isSufficientVersionOfLibcxx("cvc5jni"))
+                        || IS_WINDOWS
+                        || IS_MAC
+
+                Solvers.OPENSMT -> IS_LINUX && isSufficientVersionOfLibcxx("opensmtj")
+                Solvers.BITWUZLA -> (IS_LINUX && isSufficientVersionOfLibcxx("bitwuzlaj"))
+                        || (IS_WINDOWS && !IS_ARCH_ARM64)
+
+                Solvers.MATHSAT5 -> (IS_WINDOWS && !IS_ARCH_ARM64)
+                Solvers.Z3 -> (IS_LINUX && isSufficientVersionOfLibcxx("z3"))
+                        || IS_WINDOWS
+                        || IS_MAC
+
+                Solvers.Z3_WITH_INTERPOLATION -> IS_LINUX && !IS_ARCH_ARM64
+            }
+        }


This code is taken from SolverContextFactory and clutters up the example. Maybe there's a way to make isSupportedOperatingSystemAndArchitecture part of the JavaSMT API to avoid all the duplicate code?

baierd

Nice work, thank you!

Something to discuss (input from @kfriedberger and @PhilippWendler would be appreciated):

I noticed that we copy around files in the example projects. This might be confusing to people that use them as templates. A possible solution for this would be to extract the example projects into their own repositories and link the repositories to ours (so that they are folders that just link to the other repo).
Edit: this also seems to indicate that this would be a good idea, as it would make developing/updating in the projects easier.

baierd · 2026-06-05T10:57:47Z

+          archive: false
+
+  kotlin:
+    name: Kotlin Example Project


Adding the used build-system would be good.

I've renamed it to "Kotlin Gradle Project" now. Is that fine with you?

baierd · 2026-06-05T11:03:22Z

+      fail-fast: false
+      matrix:
+        java-version: [ 21 ]
+        os: [ubuntu-24.04, ubuntu-24.04-arm, windows-2025, windows-11-arm, macos-26-intel, macos-26]


Selecting the OS this way would require us to manually update this file every time we have a newer OS version. This might lead to this being overseen. You can just use the latest tag with wildcards, as can be seen here for example, so that we automatically use the newest OS.

I've now updated them to latest as far as possible. However, for the arm runners there is no latest release and the exact version needs to be provided (see here)

baierd · 2026-06-05T11:06:23Z

+    steps:
+      - uses: actions/checkout@v6
+
+      - name: Set up JDK ${{ matrix.java-version }}


Why not use a dependencies job as in ci.yml to set up our environment correctly, i.e. so that Java and other dependencies are present. And why don't we just extend ci.yml?

Java is fetched by actions/setup-java and we're using caches to avoid downloading the dependencies multiple times. We could try integrating it further with ci.yml, but since the examples are using various different build systems, there may not be that much overlap

In total the example-project-ci workflow takes 7-8 minutes to run, which is probably still fine, especially as we may not have to run it as often as our regular CI jobs

baierd · 2026-06-05T11:33:37Z

+  @Test
+  public void checkSudoku()
      throws InvalidConfigurationException, InterruptedException, SolverException {
+    assumeTrue(isSupportedOperatingSystemAndArchitecture(solver));


Wouldn't a @BeforeEach that checks this make more sense?

Note: and please name and document the expected behavior such that it becomes clear what went wrong fast.

The same thing applies to all test classes in this PR.

baierd · 2026-06-05T11:47:40Z

+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>


Note: applies to several files.

baierd · 2026-06-05T11:51:40Z

+
+    <target name="download-ivy" unless="skip.download">
+        <mkdir dir="lib"/>
+        <get src="https://repo1.maven.org/maven2/org/apache/ivy/ivy/2.5.0/ivy-2.5.0.jar"


We install Ivy from Maven? ;D

I think it would be better to fail instead of installing something here. You can take a look at how CPAchecker fails if Ant or Ivy are missing here.

Ivy does need to be downloaded before building as it is not included in the ant installation. However, I did change the download location to sosy-labs now

baierd · 2026-06-05T11:52:53Z

+        <ivy:retrieve pattern="lib/java/[conf]/([arch]/)[artifact](-[classifier]).[ext]"/>
+    </target>
+
+    <target name="copy" depends="resolve" description="--> copy solver libraries">


Since we usually don't want users to do this, we should document why we do it here!

…oject

daniel-raffler · 2026-06-05T15:54:23Z

+on:
+  push


We should remember to change this before merging. Right now it will trigger whenever anything is pushed to github. We could restrict it to only pushes to main, or maybe even have it manually triggered (whenever we release a new version of JavaSMT)

PhilippWendler · 2026-06-08T07:27:50Z

I noticed that we copy around files in the example projects. This might be confusing to people that use them as templates. A possible solution for this would be to extract the example projects into their own repositories and link the repositories to ours (so that they are folders that just link to the other repo).

I do not know what files you are copying around nor when, why, or how a separate repository is supposed to help with that. If you want input from me please explain the current solution and its problems.

baierd · 2026-06-08T10:59:59Z

I noticed that we copy around files in the example projects. This might be confusing to people that use them as templates. A possible solution for this would be to extract the example projects into their own repositories and link the repositories to ours (so that they are folders that just link to the other repo).

I do not know what files you are copying around nor when, why, or how a separate repository is supposed to help with that. If you want input from me please explain the current solution and its problems.

JavaSMT requires solver binaries to be in a particular location (if you don't use custom loading mechanisms). Since the example projects are located in some nested folders, we need to move the solver binaries around after we retrieved them, so that the example projects work properly. You can see this for example here. This might be confusing for users that just copy the example projects.
If we were to use dedicated repositories per example project, this problem would not exist.

PhilippWendler · 2026-06-08T11:06:11Z

If we were to use dedicated repositories per example project, this problem would not exist.

Why? How would the solver binaries end up in the example project then? And why couldn't the same mechanism be used for example projects in a subdirectory?

daniel-raffler added 26 commits March 23, 2025 15:43

Add JavaSMT project template for Ivy/Ant

7c49fa8

IvyExampleProject: Copy library files for windows

0eb0775

IvyExampleProject: Add symlinks for macOS

7cdb937

IvyExampleProject: Copy solver binaries and remove the symlinks

aec0884

IvyExampleProject: Update to latest JavaSMT release

f17ec99

Update version in the Maven example

4ba869e

Add a comment about excluding solvers in Maven or changing their vers…

e2a582e

…ion number to the example project

Add documentation about manually overriding solver versions in Ivy to…

2f8e3f6

… the starter guide

Add documentation about getting the right solver versions for Maven t…

caf79d8

…o the starter guide

Update Maven web example

3bf58a3

Update Gradle example

03f0b2d

Update Kotlin Gradle example

c191367

Remove kotlin-stdlib dependency in Kotlin Gradle example

0193b70

Use parametrized test in the Gradle example

d03c6ae

Add missing solver tests to the Kotlin example

62fe096

Rewrite test for the Kotlin example

4503a55

Update JavaSMT version in the Ivy example project

72a5ae8

Add tests for the Ivy example project and make it better aligned with…

bbcd676

… the other template projects

Merge remote-tracking branch 'refs/remotes/origin/master' into 463-pr…

b0668f4

…oblems-with-installation

Compile to Java17 in the Kotlin example

df3d41c

Print solver names while running the tests in the Kotlin example

ddd98fa

Fix macOS paths in Ivy example project

c869679

Add support for other platforms in Ivy example project

b5ca507

Add support for other platforms in example projects

ad1a139

Merge branch 'update-maven-example' into example-project-ci

c511833

Add CI for JavaSMT example projects

bb653b9

daniel-raffler self-assigned this May 30, 2026

Use junitlauncher to run tests in Ivy example project

7064468

daniel-raffler requested a review from baierd June 1, 2026 18:38

daniel-raffler commented Jun 1, 2026

View reviewed changes

baierd requested changes Jun 5, 2026

View reviewed changes

daniel-raffler added 4 commits June 5, 2026 16:25

Rename Kotlin project to "Kotlin Gradle" in the CI for the example pr…

02da8c4

…oject

Use "-latest" github runners when possible

4cf33a2

Download Ivy from sosy-labs

faae96e

Remove skip.download option

739370d

daniel-raffler commented Jun 5, 2026

View reviewed changes

daniel-raffler added 2 commits June 5, 2026 21:34

Add missing org.junit.platform dependency to the Ivy example project

034aaa3

Move platform check to @beforeeach block in project examples

7d06fd6

		on:
		push

Uh oh!

Conversation

daniel-raffler commented May 30, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

baierd left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

PhilippWendler commented Jun 8, 2026

Uh oh!

baierd commented Jun 8, 2026

Uh oh!

PhilippWendler commented Jun 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

3 participants

baierd left a comment •

edited

Loading