Update to SMTInterpol Version 2.5-1388

[baierd]

SMTInterpol is available in version 2.5-1388 while we still use the 3 year old version 2.5-1242.

I don't know the details of changes, but the new version does include changes to the proof format and potentially bitvector support.

[daniel-raffler]

I've updated the version to 2.5-1388 here and added BitVector support. Unfortunately there seem to be some strange issues when trying to use the new build with benchmark cloud. Here are some runs with different versions of SmtInterpol:

The leftmost column is with version 2.5-1242 and the rest uses 2.5-1388. For the second column I only changed the SmtInterpol version in lib/ivy.xml, and the others fix some bugs and add support for BitVectors. All of the Exceptions have the same Stacktrace:

Running CPAchecker with Java heap of size 7000M.
Running CPAchecker with default stack size (1024k). Specify a larger value with --stack if needed.
Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)

Using the following resource limits: CPU-time limit of 60s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 4.0-173-g239adf2a3f+ / bmc (OpenJDK 64-Bit Server VM 17.0.14) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "test/programs/benchmarks/bitvector/soft_float_4-2a.c.cil.c" (CPAchecker.parse, INFO)

Exception in thread "main" java.lang.NoSuchMethodError: 'boolean de.uni_freiburg.informatik.ultimate.logic.Sort.isBitVecSort()'
	at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.addTermAxioms(Clausifier.java:1099)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.createEqualityProxy(Clausifier.java:2190)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.setupCClosure(Clausifier.java:2328)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.setLogic(Clausifier.java:2531)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.setupClausifier(SMTInterpol.java:605)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.setLogic(SMTInterpol.java:581)
	at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolSolverContext.getSmtInterpolScript(SmtInterpolSolverContext.java:167)
	at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolSolverContext.create(SmtInterpolSolverContext.java:118)
	at org.sosy_lab.java_smt.SolverContextFactory.generateContext0(SolverContextFactory.java:268)
	at org.sosy_lab.java_smt.SolverContextFactory.generateContext(SolverContextFactory.java:214)
	at org.sosy_lab.cpachecker.util.predicates.smt.Solver.<init>(Solver.java:148)
	at org.sosy_lab.cpachecker.util.predicates.smt.Solver.create(Solver.java:225)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPA.<init>(PredicateCPA.java:164)
...

So there is an internal exception while initializing the solver as a (presumably new?) method can't be found. The method is clearly there, though, and I can't reproduce the crashes when running the CPAchecker command directly on my own machine (or with ssh on ubuntu2204.sosy.ifi.lmu.de). The problem also seems to be non-deterministic. Here I repeated the same run 4 times and got different results every time:

@baierd: Can you think of a way to debug this?

[daniel-raffler]

I've just run the test set with benchexec on my own computer and didn't see any of these crashes:

(The remaining Exceptions are due to SmtInterpol returning unknown for isSat and are not related to the problems on benchcloud)

[kfriedberger]

Please note that CPAchecker internally comes with identical named classes from UltimateAutomizer and this collides with JavaSMTs classes from SMTInterpol. This was also the reason why SMTInterpol was not updated for some time, because CPAchecker would crash in multiple occasions when using SMTInterpol.

The ordering of loading classes comes from "randomness" in JVM and CPAchecker, such that the error might only happen, if the Ultimate classes are loaded first (and miss new features -> NoSuchMethod).

I currently do not find the corresponding issue in CPAchecker, but is was related to a former SV-Comp, maybe 2022 or 2023.

[daniel-raffler]

Please note that CPAchecker internally comes with identical named classes from UltimateAutomizer and this collides with JavaSMTs classes from SMTInterpol. This was also the reason why SMTInterpol was not updated for some time, because CPAchecker would crash in multiple occasions when using SMTInterpol.

Thanks for the tip! That would explain these weird crashes.

I currently do not find the corresponding issue in CPAchecker, but is was related to a former SV-Comp, maybe 2022 or 2023.

CPAchecker also uses lasso-ranker, which has a dependency on SMTInterpol in version 2.5-1242-g5c50fb6d. Loading both versions at the same time probably isn't a good idea. I'll try to update these dependencies.

I currently do not find the corresponding issue in CPAchecker, but is was related to a former SV-Comp, maybe 2022 or 2023.

I think I found it here

[daniel-raffler]

I've opened an issue for SMTInterpol here:
ultimate-pa/smtinterpol#151

[daniel-raffler]

I've dug a little further and it seems that the Ultimate repository that includes lasso-ranker also comes with its own version of SMTInterpol. The version is fairly recent and there is a script to automatically update SMTInterpol to the latest release. We've so far used the standalone build from here and this is why we're having issues with colliding class files: The standalone jar includes dependencies that are also part of Ultimate and required by lasso-ranker, which leads to collisions when both are used together. When building SMTInterpol from the Ultimate repository we don't run into the same problem, and the shared classes are simply treated as dependencies.

We should therefore consider moving to the Ultimate repository for building SMTInterpol. One issue that still stands in the way is that Ultimate requires Java 21, which is much too recent for us. We could try back-porting the Ultimate repository, or maybe look for an older version that is still compatible with our version of Java to solve this problem

[daniel-raffler]

I've been able to compile SMTInterpol with Ultimate, but the process is somewhat involved:

• We need to go back to ultimate-pa/ultimate@f6a3721. This commit is about 6 month old and it is the last version of Ultimate before they switched from Java 11 to Java 21
• We haven't updated LassoRanker/Ultimate for more than 2 years and there are several new external dependencies that will have to be added to the Ivy repository:
  • ch.qos.reload4j#reload4j
  • com.sun.xml.bind#jaxb-osgi
  • net.sf.trove4j#trove4j
  • org.osgi#org.osgi.service.prefs
• Some new packages were added to Ultimate that will have to be included in our release. I've moved the entire release from de.uni-freiburg.informatik.ultimate tode.uni_freiburg.informatik.ultimate (notice the underscore) to make this change more obvious and match the structure of the Maven release. The list of modules now looks like this:

ultimate.astbuilder
ultimate.boogie.parser
ultimate.boogie.preprocessor
ultimate.boogie.printer
ultimate.core
ultimate.javacup
ultimate.lib.automata
ultimate.lib.boogieast
ultimate.lib.core
ultimate.lib.icfgtransformer
ultimate.lib.modelcheckerutils
ultimate.lib.proofs
ultimate.lib.smtlib
ultimate.lib.smtlibutils
ultimate.lib.tracecheckerutils
ultimate.lib.ultimatemodel
ultimate.lib.util
ultimate.plugins.analysis.abstractinterpretationv2
ultimate.plugins.analysis.irsdependencies
ultimate.plugins.generator.rcfgbuilder
ultimate.smtinterpol
ultimate.smtsolver.external

• Only ultimate.smtinterpol and ultimate.lib.lassoranker are meant to be used as dependencies in JavaSMT and CPAchecker for now. The other modules are dummies and don't have their dependencies properly defined yet.
• We'll use version 0.2.5-sosy0 for Ultimate and 2.5-1389 for SMTInterpol for the first release. The next release will then be 0.2.5-sosy1 for Ultimate and 2.5-139X for SMTInterpol. Both versions need to be increased simultaneously due to circular dependencies.
• We can only move past 0.2.5 for Ultimate once we migrate to Java 21

I've set up a script to help with the release here (EDIT: actually here, I messed up the Dockerfile). Here are the full build instructions:

• Create a new folder named workspace in your home directory
• Checkout SMTInterpol, Ultimate and the Ivy repository into that folder
• Copy the files from the .zip into the ivy folder
• Switch to the build container:

cd ~/workspace/ivy/release-ultimate
./buildUbuntu2204.sh
./runUbuntu2204.sh

• Fetch the external dependencies:

ant install -Dorganisation=ch.qos.reload4j -Dmodule=reload4j -Drevision=1.2.25
ant install -Dorganisation=com.sun.xml.bind -Dmodule=jaxb-osgi -Drevision=4.0.5
ant install -Dorganisation=net.sf.trove4j -Dmodule=trove4j -Drevision=3.0.3
ant install -Dorganisation=org.osgi -Dmodule=org.osgi.service.prefs -Drevision=1.1.2

• Clean up the Ivy repository (maybe?):

svn revert -R repository/

• Build and install the Ultimate packages (this will take several minutes)

./publish-ultimate.py /workspace/ultimate 0.2.5-sosy0 2.5-1389-g82bafc9c

• Use svn to commit the new files to the repository

It would be great if somebody could give this a try and make sure everything is working.

[PhilippWendler]

I would think that JavaSMT would not want to be locked into using an old SMTInterpol version for many many years, right? At the very least this needs to be explicitly discussed and decided.

[daniel-raffler]

I would think that JavaSMT would not want to be locked into using an old SMTInterpol version for many many years, right? At the very least this needs to be explicitly discussed and decided.

Just to clarify: We could continue to update SMTInterpol, it's LassoRanker (and the rest of Ultimate) that will be stuck at version 0.2.5 as newer version require Java 21.

There is actually a PR for Ultimate that would make SMTInterpol a dependency here, and this would likely solve our issues. However, I'm not sure when/if it will go through, and we would have to wait for CPAchecker to transition to Java 21 before we can use it.

[PhilippWendler]

I would think that JavaSMT would not want to be locked into using an old SMTInterpol version for many many years, right? At the very least this needs to be explicitly discussed and decided.

Just to clarify: We could continue to update SMTInterpol, it's LassoRanker (and the rest of Ultimate) that will be stuck at version 0.2.5 as newer version require Java 21.

My understanding is that this PR would force JavaSMT to use an old SMTInterpol version, and only without this PR JavaSMT could update SMTInterpol without requiring Java 21, is this correct?

[daniel-raffler]

I would think that JavaSMT would not want to be locked into using an old SMTInterpol version for many many years, right? At the very least this needs to be explicitly discussed and decided.

Just to clarify: We could continue to update SMTInterpol, it's LassoRanker (and the rest of Ultimate) that will be stuck at version 0.2.5 as newer version require Java 21.

My understanding is that this PR would force JavaSMT to use an old SMTInterpol version, and only without this PR JavaSMT could update SMTInterpol without requiring Java 21, is this correct?

We would commit to version 0.2.5 of Ultimate, which does contain its own version of SMTInterpol. However, this version can be updated independently using a script (link, and here for the manual instructions) that is included with Ultimate. I've tried it and was able to update SMTInterpol from the version that is included with Ultimate 0.2.5 to the most recent release (~ 9 months worth of changes) without any major issues. If SMTInterpol makes any API braking changes to their version of Library-SMTLIB things might get more complicated. However, such changes seem to be rare and we shouldn't have any issues back-porting minor fixes.