Merge remote-tracking branch 'origin/master' into update_z3-4.15.3

Author: kfriedberger

.classpath

@@ -21,7 +21,7 @@ SPDX-License-Identifier: Apache-2.0
 	<classpathentry kind="lib" path="lib/java/core/spotbugs-annotations.jar" sourcepath="lib/java-contrib/spotbugs-annotations-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/core/jsr305.jar" sourcepath="lib/java-contrib/jsr305-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/build/auto-value-annotations.jar"/>
-	<classpathentry kind="lib" path="lib/java/core/error_prone_annotations.jar" sourcepath="lib/java-contrib/error_prone_annotations-sources.jar"/>
+	<classpathentry kind="lib" path="lib/java/build/error_prone_annotations.jar" sourcepath="lib/java-contrib/error_prone_annotations-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/core/common.jar" sourcepath="lib/java-contrib/common-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime-smtinterpol/smtinterpol.jar" sourcepath="lib/java-contrib/smtinterpol-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime-princess/princess_2.13.jar" sourcepath="lib/java-contrib/princess_2.13-sources.jar"/>

.gitlab-ci.yml

@@ -12,6 +12,6 @@ variables:
   PROJECT_PATH: "sosy-lab/software/java-smt"
   GH_REF: "github.com/sosy-lab/java-smt"
   # Version of https://gitlab.com/sosy-lab/software/refaster/ to use
-  REFASTER_REPO_REVISION: 31cd8ffc4966957e156665dbba76679ade5bb5c9
+  REFASTER_REPO_REVISION: 26c8309d1023e4dfcb0e8d24dcf7ec12e621314e
   # Needs to be synchronized with Error Prone version in lib/ivy.xml
-  REFASTER_VERSION: 2.21.1
+  REFASTER_VERSION: 2.41.0

.settings/org.eclipse.jdt.core.prefs

@@ -2,11 +2,12 @@
 # an API wrapper for a collection of SMT solvers:
 # https://github.com/sosy-lab/java-smt
 #
-# SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+# SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 #
 # SPDX-License-Identifier: Apache-2.0
 
 eclipse.preferences.version=1
+org.eclipse.jdt.core.builder.annotationPath.allLocations=disabled
 org.eclipse.jdt.core.codeComplete.argumentPrefixes=p
 org.eclipse.jdt.core.codeComplete.argumentSuffixes=
 org.eclipse.jdt.core.codeComplete.fieldPrefixes=
@@ -23,9 +24,12 @@ org.eclipse.jdt.core.compiler.annotation.nonnull=javax.annotation.Nonnull
 org.eclipse.jdt.core.compiler.annotation.nonnull.secondary=
 org.eclipse.jdt.core.compiler.annotation.nonnullbydefault=org.sosy_lab.common.annotations.FieldsAreNonnullByDefault
 org.eclipse.jdt.core.compiler.annotation.nonnullbydefault.secondary=
+org.eclipse.jdt.core.compiler.annotation.notowning=org.eclipse.jdt.annotation.NotOwning
 org.eclipse.jdt.core.compiler.annotation.nullable=javax.annotation.Nullable
 org.eclipse.jdt.core.compiler.annotation.nullable.secondary=
 org.eclipse.jdt.core.compiler.annotation.nullanalysis=disabled
+org.eclipse.jdt.core.compiler.annotation.owning=org.eclipse.jdt.annotation.Owning
+org.eclipse.jdt.core.compiler.annotation.resourceanalysis=disabled
 org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
 org.eclipse.jdt.core.compiler.codegen.methodParameters=do not generate
 org.eclipse.jdt.core.compiler.codegen.targetPlatform=11
@@ -36,6 +40,7 @@ org.eclipse.jdt.core.compiler.debug.localVariable=generate
 org.eclipse.jdt.core.compiler.debug.sourceFile=generate
 org.eclipse.jdt.core.compiler.doc.comment.support=enabled
 org.eclipse.jdt.core.compiler.problem.APILeak=warning
+org.eclipse.jdt.core.compiler.problem.annotatedTypeArgumentToUnannotated=info
 org.eclipse.jdt.core.compiler.problem.annotationSuperInterface=ignore
 org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
 org.eclipse.jdt.core.compiler.problem.autoboxing=ignore
@@ -57,8 +62,10 @@ org.eclipse.jdt.core.compiler.problem.forbiddenReference=error
 org.eclipse.jdt.core.compiler.problem.hiddenCatchBlock=warning
 org.eclipse.jdt.core.compiler.problem.includeNullInfoFromAsserts=enabled
 org.eclipse.jdt.core.compiler.problem.incompatibleNonInheritedInterfaceMethod=warning
+org.eclipse.jdt.core.compiler.problem.incompatibleOwningContract=warning
 org.eclipse.jdt.core.compiler.problem.incompleteEnumSwitch=warning
 org.eclipse.jdt.core.compiler.problem.indirectStaticAccess=warning
+org.eclipse.jdt.core.compiler.problem.insufficientResourceAnalysis=warning
 org.eclipse.jdt.core.compiler.problem.invalidJavadoc=warning
 org.eclipse.jdt.core.compiler.problem.invalidJavadocTags=enabled
 org.eclipse.jdt.core.compiler.problem.invalidJavadocTagsDeprecatedRef=disabled
@@ -88,14 +95,14 @@ org.eclipse.jdt.core.compiler.problem.nonExternalizedStringLiteral=ignore
 org.eclipse.jdt.core.compiler.problem.nonnullParameterAnnotationDropped=warning
 org.eclipse.jdt.core.compiler.problem.nonnullTypeVariableFromLegacyInvocation=warning
 org.eclipse.jdt.core.compiler.problem.nullAnnotationInferenceConflict=error
-org.eclipse.jdt.core.compiler.problem.nullReference=warning
+org.eclipse.jdt.core.compiler.problem.nullReference=error
 org.eclipse.jdt.core.compiler.problem.nullSpecViolation=error
 org.eclipse.jdt.core.compiler.problem.nullUncheckedConversion=warning
 org.eclipse.jdt.core.compiler.problem.overridingPackageDefaultMethod=warning
 org.eclipse.jdt.core.compiler.problem.parameterAssignment=ignore
 org.eclipse.jdt.core.compiler.problem.pessimisticNullAnalysisForFreeTypeVariables=warning
 org.eclipse.jdt.core.compiler.problem.possibleAccidentalBooleanAssignment=warning
-org.eclipse.jdt.core.compiler.problem.potentialNullReference=warning
+org.eclipse.jdt.core.compiler.problem.potentialNullReference=error
 org.eclipse.jdt.core.compiler.problem.potentiallyUnclosedCloseable=warning
 org.eclipse.jdt.core.compiler.problem.rawTypeReference=warning
 org.eclipse.jdt.core.compiler.problem.redundantNullAnnotation=warning
@@ -108,14 +115,15 @@ org.eclipse.jdt.core.compiler.problem.specialParameterHidingField=disabled
 org.eclipse.jdt.core.compiler.problem.staticAccessReceiver=warning
 org.eclipse.jdt.core.compiler.problem.suppressOptionalErrors=enabled
 org.eclipse.jdt.core.compiler.problem.suppressWarnings=enabled
+org.eclipse.jdt.core.compiler.problem.suppressWarningsNotFullyAnalysed=ignore
 org.eclipse.jdt.core.compiler.problem.syntacticNullAnalysisForFields=disabled
 org.eclipse.jdt.core.compiler.problem.syntheticAccessEmulation=ignore
 org.eclipse.jdt.core.compiler.problem.terminalDeprecation=warning
 org.eclipse.jdt.core.compiler.problem.typeParameterHiding=warning
 org.eclipse.jdt.core.compiler.problem.unavoidableGenericTypeProblems=enabled
 org.eclipse.jdt.core.compiler.problem.uncheckedTypeOperation=warning
 org.eclipse.jdt.core.compiler.problem.unclosedCloseable=warning
-org.eclipse.jdt.core.compiler.problem.undocumentedEmptyBlock=ignore
+org.eclipse.jdt.core.compiler.problem.undocumentedEmptyBlock=info
 org.eclipse.jdt.core.compiler.problem.unhandledWarningToken=ignore
 org.eclipse.jdt.core.compiler.problem.unlikelyCollectionMethodArgumentType=warning
 org.eclipse.jdt.core.compiler.problem.unlikelyCollectionMethodArgumentTypeStrict=disabled
@@ -128,9 +136,10 @@ org.eclipse.jdt.core.compiler.problem.unusedDeclaredThrownException=warning
 org.eclipse.jdt.core.compiler.problem.unusedDeclaredThrownExceptionExemptExceptionAndThrowable=enabled
 org.eclipse.jdt.core.compiler.problem.unusedDeclaredThrownExceptionIncludeDocCommentReference=enabled
 org.eclipse.jdt.core.compiler.problem.unusedDeclaredThrownExceptionWhenOverriding=disabled
-org.eclipse.jdt.core.compiler.problem.unusedExceptionParameter=ignore
+org.eclipse.jdt.core.compiler.problem.unusedExceptionParameter=info
 org.eclipse.jdt.core.compiler.problem.unusedImport=warning
 org.eclipse.jdt.core.compiler.problem.unusedLabel=warning
+org.eclipse.jdt.core.compiler.problem.unusedLambdaParameter=warning
 org.eclipse.jdt.core.compiler.problem.unusedLocal=warning
 org.eclipse.jdt.core.compiler.problem.unusedObjectAllocation=warning
 org.eclipse.jdt.core.compiler.problem.unusedParameter=warning
@@ -139,7 +148,7 @@ org.eclipse.jdt.core.compiler.problem.unusedParameterWhenImplementingAbstract=di
 org.eclipse.jdt.core.compiler.problem.unusedParameterWhenOverridingConcrete=disabled
 org.eclipse.jdt.core.compiler.problem.unusedPrivateMember=warning
 org.eclipse.jdt.core.compiler.problem.unusedTypeParameter=warning
-org.eclipse.jdt.core.compiler.problem.unusedWarningToken=ignore
+org.eclipse.jdt.core.compiler.problem.unusedWarningToken=info
 org.eclipse.jdt.core.compiler.problem.varargsArgumentNeedCast=warning
 org.eclipse.jdt.core.compiler.processAnnotations=enabled
 org.eclipse.jdt.core.compiler.release=enabled

build/build-compile.xml

@@ -36,9 +36,10 @@ SPDX-License-Identifier: Apache-2.0
         <exclude name="**/*.java" />
     </patternset>
 
-    <!-- error-prone config from https://errorprone.info/docs/installation#jdk-16 -->
+    <!-- error-prone config from https://errorprone.info/docs/installation#ant -->
     <property name="errorprone.options.required" value="
         -XDcompilePolicy=simple
+        --should-stop=ifError=FLOW
         -J--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED
         -J--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED
         -J--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED
@@ -55,6 +56,11 @@ SPDX-License-Identifier: Apache-2.0
       <javaversion atleast="21"/>
     </condition>
 
+    <!-- Current versions of Error Prone do not support running on Java 11 anymore. -->
+    <condition property="errorprone.disable">
+      <javaversion exactly="11"/>
+    </condition>
+
     <!-- We use error-prone as the compiler, cf. http://errorprone.info/ -->
     <target name="build-project" unless="skipBuild" depends="build-dependencies">
         <depend srcdir="${source.dir}" destdir="${class.dir}"/>
@@ -74,7 +80,7 @@ SPDX-License-Identifier: Apache-2.0
             <src path="${source.dir}"/>
             <classpath refid="classpath"/>
             <compilerarg value="-Xlint"/>
-            <compilerarg value="-Xlint:-fallthrough"/> <!-- checked by error-prone, too, and javac does not recognize $FALL-THROUGH$ -->
+            <compilerarg value="-Xlint:-fallthrough"/> <!-- checked by error-prone, too, and javac does not recognized $FALL-THROUGH$ -->
             <compilerarg value="-Xlint:-processing"/>
             <compilerarg value="-Xlint:-options"/> <!-- suppress warning about bootclasspath on newer JDK -->
             <compilerarg value="-Xlint:-this-escape" if:set="java21"/> <!-- false alarm for every use of configuration injection -->
@@ -130,11 +136,14 @@ SPDX-License-Identifier: Apache-2.0
         <mkdir dir="${source.generated.dir}"/>
 
         <copy file=".settings/org.eclipse.jdt.core.prefs" tofile="${ivy.lib.dir}/build/org.eclipse.jdt.core.prefs">
-            <!-- Convert all compiler warnings to errors. -->
+            <!-- Convert all compiler warnings to errors and ignore info messages to not clutter the output. -->
             <filterchain>
                 <replacetokens begintoken="=" endtoken="g">
                     <token key="warnin" value="=error"/>
                 </replacetokens>
+                <replacetokens begintoken="=" endtoken="o">
+                    <token key="inf" value="=ignore"/>
+                </replacetokens>
             </filterchain>
         </copy>
 

build/build-documentation.xml

@@ -37,7 +37,7 @@ SPDX-License-Identifier: Apache-2.0
 
             <classpath refid="classpath"/>
 
-            <!-- "-v" is an optional param for verbose output of OptionCollector -->
+            <!-- "-v" is a optional param for verbose output of OptionCollector -->
             <!-- <arg value="-v"/> -->
         </java>
         <echo message="Options collected." level="info"/>

build/build-ivy.xml

@@ -46,7 +46,7 @@ SPDX-License-Identifier: Apache-2.0
     </condition>
     <property name="ivy.cache.dir" location="${tmp.ivy.cache.dir}" />
 
-    <!-- If necessary, download Ivy from website so that it does not need to be installed. -->
+    <!-- If necessary, download Ivy from web site so that it does not need to be installed. -->
     <target name="bootstrap-ivy" unless="ivy.jar.present">
         <mkdir dir="${ivy.jar.dir}"/>
         <echo message="Downloading ivy..."/>

build/gitlab-ci.Dockerfile.jdk-11

@@ -6,13 +6,13 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-# This is a Docker image for running the tests.
+# This is a container image for running the tests.
 # It should be pushed to registry.gitlab.com/sosy-lab/software/java-smt/test
 # and will be used by CI as declared in .gitlab-ci.yml.
 #
 # Commands for updating the image:
-# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-11 - < build/gitlab-ci.Dockerfile.jdk-11
-# docker push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-11
+# podman build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-11 - < build/gitlab-ci.Dockerfile.jdk-11
+# podman push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-11
 
 FROM ubuntu:20.04
 

build/gitlab-ci.Dockerfile.jdk-17

@@ -6,13 +6,13 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-# This is a Docker image for running the tests.
+# This is a container image for running the tests.
 # It should be pushed to registry.gitlab.com/sosy-lab/software/java-smt/test
 # and will be used by CI as declared in .gitlab-ci.yml.
 #
 # Commands for updating the image:
-# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-17 - < build/gitlab-ci.Dockerfile.jdk-17
-# docker push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-17
+# podman build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-17 - < build/gitlab-ci.Dockerfile.jdk-17
+# podman push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-17
 
 FROM ubuntu:20.04
 

build/gitlab-ci.Dockerfile.jdk-21

@@ -6,13 +6,13 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-# This is a Docker image for running the tests.
+# This is a container image for running the tests.
 # It should be pushed to registry.gitlab.com/sosy-lab/software/java-smt/test
 # and will be used by CI as declared in .gitlab-ci.yml.
 #
 # Commands for updating the image:
-# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-21 - < build/gitlab-ci.Dockerfile.jdk-21
-# docker push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-21
+# podman build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-21 - < build/gitlab-ci.Dockerfile.jdk-21
+# podman push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-21
 
 FROM ubuntu:20.04
 

build/gitlab-ci.Dockerfile.jdk-23 renamed to build/gitlab-ci.Dockerfile.jdk-24

@@ -6,16 +6,16 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-# This is a Docker image for running the tests.
+# This is a container image for running the tests.
 # It should be pushed to registry.gitlab.com/sosy-lab/software/java-smt/test
 # and will be used by CI as declared in .gitlab-ci.yml.
 #
 # Commands for updating the image:
-# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-23 - < build/gitlab-ci.Dockerfile.jdk-23
-# docker push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-23
+# podman build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-24 - < build/gitlab-ci.Dockerfile.jdk-24
+# podman push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-24
 
-# Older Ubuntu versions currently do not have GLIC_2.34 and Java 23
-FROM ubuntu:24.10
+# LTS versions currently do not have Java 24
+FROM ubuntu:25.04
 
 ENV DEBIAN_FRONTEND=noninteractive
 ENV TZ=UTC
@@ -25,9 +25,11 @@ RUN apt-get update && apt-get install -y --no-install-recommends \
   curl \
   git \
   jq \
-  openjdk-23-jdk-headless \
+  openjdk-24-jdk-headless \
   wget \
   && rm -rf /var/lib/apt/lists/*
 
+ENV LANG C.UTF-8
+
 RUN apt-get update && apt-get install -y \
   libgomp1