Merge remote-tracking branch 'origin/master' into use_solver_native_bv_to_ieee-fp_CVC4_CVC5

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

README.md

@@ -60,19 +60,19 @@ Only a few SMT solvers provide support for theories like Arrays, Floating Point,
 
 JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation):
 
-| SMT Solver |       Linux x64       |     Linux arm64     | Windows x64 | Windows arm64 |                       MacOS x64                        | MacOS arm64 | Description |
-| --- |:---------------------:|:-------------------:|:---:|:---:|:------------------------------------------------------:|:---:|:--- |
-| [Bitwuzla](https://bitwuzla.github.io/) |  :heavy_check_mark:²  | :heavy_check_mark:² | :heavy_check_mark: |  |                                                        |  | a fast solver for bitvector logic |
-| [Boolector](https://boolector.github.io/) |  :heavy_check_mark:   |                     |  |  |                                                        |  | a fast solver for bitvector logic, misses formula introspection, deprecated |
-| [CVC4](https://cvc4.github.io/) |  :heavy_check_mark:   |                     |  |  |                                                        |  |  |
-| [CVC5](https://cvc5.github.io/) |  :heavy_check_mark:  |  :heavy_check_mark:  |  :heavy_check_mark:  |  |  :heavy_check_mark:  |  :heavy_check_mark:  |  |
-| [MathSAT5](http://mathsat.fbk.eu/) |  :heavy_check_mark:   | :heavy_check_mark:  | :heavy_check_mark: |  | [maybe](https://github.com/sosy-lab/java-smt/pull/430)³ |  |  |
-| [OpenSMT](https://verify.inf.usi.ch/opensmt) |  :heavy_check_mark:²  | :heavy_check_mark:² |  |  |                                                        |  |  |
-| [OptiMathSAT](http://optimathsat.disi.unitn.it/) |  :heavy_check_mark:   |                     |  |  |                                                        |  | based on MathSAT5, with support for optimization queries |
-| [Princess](http://www.philipp.ruemmer.org/princess.shtml) |  :heavy_check_mark:   | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                   | :heavy_check_mark: | Java-based SMT solver |
-| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) |  :heavy_check_mark:   | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                   | :heavy_check_mark: | Java-based SMT solver |
-| [Yices2](https://yices.csl.sri.com/) |  :heavy_check_mark:   |                     | [maybe](https://github.com/sosy-lab/java-smt/pull/215) |  | [maybe](https://github.com/sosy-lab/java-smt/pull/400)³ |  |  |
-| [Z3](https://github.com/Z3Prover/z3) |  :heavy_check_mark:²  | :heavy_check_mark:² | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                   | :heavy_check_mark: | mature and well-known solver |
+| SMT Solver | Linux x64 | Linux arm64 | Windows x64 | Windows arm64 | MacOS x64 | MacOS arm64 | Description |
+| --- |:---:|:---:|:---:|:---:|:---:|:---:|:--- |
+| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark:² | :heavy_check_mark:² | :heavy_check_mark: |  |  |  | a fast solver for bitvector logic |
+| [Boolector](https://boolector.github.io/) | :heavy_check_mark: |  |  |  |  |  | a fast solver for bitvector logic, misses formula introspection, deprecated |
+| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: |  |  |  |  |  |  |
+| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: |  | :heavy_check_mark: | :heavy_check_mark: |  |
+| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: |  | [maybe](https://github.com/sosy-lab/java-smt/pull/430)⁴ |  |  |
+| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark:² | :heavy_check_mark:² |  |  |  |  |  |
+| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: |  |  |  |  |  | based on MathSAT5, with support for optimization queries |
+| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
+| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
+| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: |  | [maybe](https://github.com/sosy-lab/java-smt/pull/215) |  | [maybe](https://github.com/sosy-lab/java-smt/pull/400)⁴ |  |  |
+| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver |
 
 We support a reasonable list of operating systems and versions.
 - Our main target is Linux (mainly Ubuntu or comparable Linux distributions).
@@ -88,7 +88,9 @@ available with Ubuntu 18.04 or later.
 
 ² Solver requires at least `GLIBC_2.29`/`GLIBCXX_3.4.26` or `GLIBC_2.34`/`GLIBCXX_3.4.29`,
 available with Ubuntu 22.04 or later.  
-³ We do not provide a signed solver library for macOS. The user needs to compile and sign it.
+³ Solver requires at least `GLIBC_2.38`/`GLIBCXX_3.4.31`,
+available with Ubuntu 24.04 or later.  
+⁴ We do not provide a signed solver library for macOS. The user needs to compile and sign it.
 
 #### Solver Features
 
@@ -109,7 +111,7 @@ If something specific is missing, please [look for or file an issue](https://git
 
 #### Multithreading Support
 
-| SMT Solver | Concurrent context usage⁴ | Concurrent prover usage⁵ |
+| SMT Solver | Concurrent context usage⁵ | Concurrent prover usage⁶ |
 | --- |:---:|:---:|
 | [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: |  |
 | [Boolector](https://boolector.github.io/) | :heavy_check_mark: |  |
@@ -126,13 +128,13 @@ If something specific is missing, please [look for or file an issue](https://git
 Interruption using a [ShutdownNotifier][] may be used to interrupt a solver from any thread.
 Formulas are translatable in between contexts/provers/threads using _FormulaManager.translateFrom()_.
 
-⁴ Multiple contexts, but all operations on each context only from a single thread.  
-⁵ Multiple provers on one or more contexts, with each prover using its own thread.
+⁵ Multiple contexts, but all operations on each context only from a single thread.  
+⁶ Multiple provers on one or more contexts, with each prover using its own thread.
 
 #### Garbage Collection in Native Solvers
 
 JavaSMT exposes an API for performing garbage collection on solvers implemented in a native language.
-As a native solver has no way of knowing whether the created formula object is still referenced 
+As a native solver has no way of knowing whether the created formula object is still referenced
 by the client application, this API is necessary to avoid leaking memory.
 Note that several solvers already support _hash consing_ and thus,
 there is never more than one copy of an identical formula object in memory.
@@ -141,9 +143,9 @@ in the application, it is not necessary to perform any garbage collection at all
 Additionally, the memory for formulas created on user-side (i.e., via JavaSMT) is negligible
 compared to solver-internal memory-consumption when solving a hard SMT query.
 
-- **Z3**: The parameter `solver.z3.usePhantomReferences` may be used to control 
-  whether JavaSMT will attempt to decrease references on Z3 formula 
-  objects once they are no longer referenced.
+- **Z3**: The parameter `solver.z3.usePhantomReferences` may be used to control
+  whether JavaSMT will attempt to decrease references on Z3 formula objects
+  once they are no longer referenced.
 - **MathSAT5**: Currently we do not support performing garbage collection for MathSAT5.
 - **CVC4, CVC5, Bitwuzla, OpenSMT**: Solvers using SWIG bindings do perform garbage collection.
 - **Other native SMT solvers**: we do not perform garbage collection.

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..."/>