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: https://github.com/ultimate-pa/smtinterpol/issues/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 https://github.com/ultimate-pa/ultimate/commit/f6a3721f1dd6923f8d30cdbc29478c49096f1bd7. 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.

[PhilippWendler]

Sorry, I am not sure I understand this. I think this needs a clear description of the different options such that an informed decision can be made by the JavaSMT maintainers.

Is the following correct?

1. Current option is to take SMTInterpol from its official source. JavaSMT can easily update it whenever it wants and has little effort. The only known disadvantage is that users of JavaSMT who also happen to use Ultimate can have problems with duplicate classes.
2. New option is to take SMTInterpol from a different source, specifically from within Ultimate. This changes how SMTInterpol is packaged (how exactly?) and makes it possible for users of JavaSMT to also use Ultimate easily, if they happen to want to use the same version of Ultimate that JavaSMT uses as source for SMTInterpol. This version of Ultimate is already 6 months old and JavaSMT will be stuck with it for something on the order of a few years (a policy for updating the minimum Java version for JavaSMT is not yet defined, nor a plan for raising this version to Java 17 let alone to Java 21). JavaSMT could still try to combine newer versions of SMTInterpol with that old version of Ultimate, a combination that is not expected to be done by neither the developers of Ultimate nor those of SMTInterpol and would need to potentially even change and fork SMTInterpol and maintain that fork that remains compatible with Ultimate 0.2.5. Users of JavaSMT would not be able to use SMTInterpol but this local fork.

Did I miss something? Please add more information.

Important questions to clarify before working on this are also

• Is there any noticeable change for users when switching to "SMTInterpol from Ultimate", and what? I guess at least the packaging change must be visible somehow?
• What would a change back to plain SMTInterpol entail in terms of effort and noticeable changes for users? Could this change be done anytime?

[daniel-raffler]

I think this needs a clear description of the different options such that an informed decision can be made by the JavaSMT maintainers.

I think there are 3 options here:

1. Keep it as it is and continue with the old version of SMTInterpol
2. Switch to Ultimate for building SMTInterpol as outlined here
3. Wait for this PR to be merged before updating SMTInterpol (and LassoRanker)

The last option will only work once CPAchecker has moved to Java 21 and I don't know when/if the PR will actually be merged. It's also possible to go with option 2 now and then later switch to 3.

Is the following correct? 1. Current option is to take SMTInterpol from its official source. JavaSMT can easily update it whenever it wants and has little effort. The only known disadvantage is that users of JavaSMT who also happen to use Ultimate can have problems with duplicate classes.

I feel you're underselling the issue here: SMTInterpol has not been updated in JavaSMT for more than two years as that would break CPAchecker due to the duplicate classes problem. The same goes for LassoRanker in CPAchecker, which is also using a two year old version that can't be updated.

2. New option is to take SMTInterpol from a different source, specifically from within Ultimate. This changes how SMTInterpol is packaged (how exactly?) and makes it possible for users of JavaSMT to also use Ultimate easily, if they happen to want to use the same version of Ultimate that JavaSMT uses as source for SMTInterpol. This version of Ultimate is already 6 months old and JavaSMT will be stuck with it for something on the order of a few years (a policy for updating the minimum Java version for JavaSMT is not yet defined, nor a plan for raising this version to Java 17 let alone to Java 21). JavaSMT could still try to combine newer versions of SMTInterpol with that old version of Ultimate, a combination that is not expected to be done by neither the developers of Ultimate nor those of SMTInterpol and would need to potentially even change and fork SMTInterpol and maintain that fork that remains compatible with Ultimate 0.2.5. Users of JavaSMT would not be able to use SMTInterpol but this local fork.

SMTInterpol and Ultimate both have their own copy of the Library-SMTLIB folder, see here for SMTInterpol and here for Ultimate. The folder was originally part of SMTInterpol and contains classes like Term or Theory that are pretty general and used by both SMTInterpol and LassoRanker. Ultimate copied the folder as they needed some modifications that were not accepted upstream. Because of this there are now two versions of the same classes, which leads to issues whenever Ultimate and SMTInterpol are used together in the same project.

Building SMTInterpol as part of Ultimate solves the issue by combing both versions of .Library-SMTLIB and making SMTInterpol and Ultimate use the same classes again.

Important questions to clarify before working on this are also

• Is there any noticeable change for users when switching to "SMTInterpol from Ultimate", and what? I guess at least the packaging change must be visible somehow?

No, it should be enough to update the dependency for SMTInterpol in JavaSMT (and LassoRanker in CPAchecker)

Note that the build script currently renames some packages and moves everything from de.uni-freiburg.informatik.ultimate to de.uni_freiburg.informatik.ultimate (note the underscore). However, this was done only for convenience/consistency and we could continue to use the old package names if that is preferred.

• What would a change back to plain SMTInterpol entail in terms of effort and noticeable changes for users? Could this change be done anytime?

We should be able to switch back to the plain version of SMTInterpol once this has been merged. We would then again have to update the version of SMTInterpol in JavaSMT and LassoRanker in CPAchecker.

Note that this is only possible after CPAchecker has switched to Java 21 as Ultimate 0.2.5 is the last version that will work with older JDKs.

[baierd]

I am very much in favor of 2. (Switch to Ultimate for building SMTInterpol), as there is another branch that will use/import Ultimate anyways!

[baierd]

Would that mean we need to switch to Java 21?

[daniel-raffler]

Would that mean we need to switch to Java 21?

Option 2 will run on Java 11. If we go with option 3 SMTInterpol should still work with Java 11, but we may need Java 21 if other parts of Ultimate are used in JavaSMT.

[PhilippWendler]

I think there are 3 options here:

1. Keep it as it is and continue with the old version of SMTInterpol

I do not see how this can be an option, and as a user of JavaSMT, I am actually surprised that SMTInterpol was not updated for several years in JavaSMT.

2. Switch to Ultimate for building SMTInterpol as outlined here

3. Wait for this PR to be merged before updating SMTInterpol (and LassoRanker)

It seems clear that this PR will not be merged, and if it is, Ultimate will use a fork of SMTInterpol and not the official SMTInterpol that should be used by JavaSMT.

Why do you not list "take SMTInterpol from its official source" as an option?

Is the following correct?

1. Current option is to take SMTInterpol from its official source. JavaSMT can easily update it whenever it wants and has little effort. The only known disadvantage is that users of JavaSMT who also happen to use Ultimate can have problems with duplicate classes.

I feel you're underselling the issue here: SMTInterpol has not been updated in JavaSMT for more than two years as that would break CPAchecker due to the duplicate classes problem.

I was not aware of this, and I would certainly have said that JavaSMT should not delayed updating one of its important solvers for years. As mentioned above, as a user of JavaSMT I expect regular updates of the solvers.

2. New option is to take SMTInterpol from a different source, specifically from within Ultimate. This changes how SMTInterpol is packaged (how exactly?) and makes it possible for users of JavaSMT to also use Ultimate easily, if they happen to want to use the same version of Ultimate that JavaSMT uses as source for SMTInterpol. This version of Ultimate is already 6 months old and JavaSMT will be stuck with it for something on the order of a few years (a policy for updating the minimum Java version for JavaSMT is not yet defined, nor a plan for raising this version to Java 17 let alone to Java 21). JavaSMT could still try to combine newer versions of SMTInterpol with that old version of Ultimate, a combination that is not expected to be done by neither the developers of Ultimate nor those of SMTInterpol and would need to potentially even change and fork SMTInterpol and maintain that fork that remains compatible with Ultimate 0.2.5. Users of JavaSMT would not be able to use SMTInterpol but this local fork.

SMTInterpol and Ultimate both have their own copy of the Library-SMTLIB folder, see here for SMTInterpol and here for Ultimate. The folder was originally part of SMTInterpol and contains classes like Term or Theory that are pretty general and used by both SMTInterpol and LassoRanker. Ultimate copied the folder as they needed some modifications that were not accepted upstream. Because of this there are now two versions of the same classes, which leads to issues whenever Ultimate and SMTInterpol are used together in the same project.

Building SMTInterpol as part of Ultimate solves the issue by combing both versions of Library-SMTLIB and making SMTInterpol and Ultimate use the same classes again.

How would this "combine" anything? Wouldn't this simply mean that everything from Ultimate is used and nothing from SMTInterpol, i.e., JavaSMT would be using an unofficial variant of SMTInterpol with some core classes replaced by implementations from a different project?

As far as I understand now I think you are misrepresenting what is done when you say "building SMTInterpol from the Ultimate repository". This makes it sound that what is used is still SMTInterpol, just with some kind of different build context or so. But the Ultimate PR that you linked makes it seem that what is actually happening instead is that we would not build SMTInterpol anymore, but Ultimate's fork of it. Please make sure to keep that clear.

The SMTInterpol developers might (understandably) not like if JavaSMT publishes and publicizes a fork of SMTInterpol under the name SMTInterpol and makes it look like the official SMTInterpol. And in fact it would not even be the Ultimate fork of SMTInterpol, it would be the SoSy-Lab fork of the Ultimate fork of SMTInterpol (because we would need to do backporting).

The linked PR also makes it clear that the Ultimate people do this precisely because they want and expect to use SMTInterpol with actual modifications, e.g., prototype code of ongoing experiments and so on.

To me these are quite strong arguments against JavaSMT adopting the Ultimate fork of SMTInterpol.

Note that the build script currently renames some packages and moves everything from de.uni-freiburg.informatik.ultimate to de.uni_freiburg.informatik.ultimate (note the underscore). However, this was done only for convenience/consistency and we could continue to use the old package names if that is preferred.

Wait, what do you mean here? Which version of SMTInterpol uses which package names? What is "the build script" that you are referring to? And hyphens are not even allowed in Java packages AFAIK?

---

I am very much in favor of 2. (Switch to Ultimate for building SMTInterpol), as there is another branch that will use/import Ultimate anyways!

How will that work if Ultimate requires Java 21? Are you planning a multi-release JAR of JavaSMT such that users on Java 21 get to make use of Eliminator where as users on Java 11 or 17 get a version of JavaSMT without that feature?

[daniel-raffler]

Why do you not list "take SMTInterpol from its official source" as an option?

That's what I tried initially and it caused random crashes in CPAchecker due to the duplicate class issue (see the top of this thread here). As we need CPAchecker to work on benchcloud this seemed like a show stopper to me.

How would this "combine" anything? Wouldn't this simply mean that everything from Ultimate is used and nothing from SMTInterpol, i.e., JavaSMT would be using an unofficial variant of SMTInterpol with some core classes replaced by implementations from a different project?

From what I understand the update script used by Ultimate (here and here) effectively merges the changes from both versions.

As far as I understand now I think you are misrepresenting what is done when you say "building SMTInterpol from the Ultimate repository". This makes it sound that what is used is still SMTInterpol, just with some kind of different build context or so. But the Ultimate PR that you linked makes it seem that what is actually happening instead is that we would not build SMTInterpol anymore, but Ultimate's fork of it. Please make sure to keep that clear.

The SMTInterpol developers might (understandably) not like if JavaSMT publishes and publicizes a fork of SMTInterpol under the name SMTInterpol and makes it look like the official SMTInterpol. And in fact it would not even be the Ultimate fork of SMTInterpol, it would be the SoSy-Lab fork of the Ultimate fork of SMTInterpol (because we would need to do backporting).

That's a fair point. I did already rename the ivy module from smtinterpol to ultimate.smtinterpol, but we could still add a -sosyX tag to the version to make the difference more clear.

Note that the build script currently renames some packages and moves everything from de.uni-freiburg.informatik.ultimate to de.uni_freiburg.informatik.ultimate (note the underscore). However, this was done only for convenience/consistency and we could continue to use the old package names if that is preferred.

Wait, what do you mean here? Which version of SMTInterpol uses which package names? What is "the build script" that you are referring to? And hyphens are not even allowed in Java packages AFAIK?

I meant the Ivy module names, and the new version here uses de.uni_freiburg.informatik.ultimate with an underscore. The package names in Java are unchanged and only ivy.xml will have to be updated for JavaSMT and CPAchecker.

You can find the "build script" for publishing Ultimate/SMTInterpol to Ivy here. Is there a way to open PRs for the Sosy Ivy repository? It would probably be better to move that discussion somewhere else.

[PhilippWendler]

Why do you not list "take SMTInterpol from its official source" as an option?

That's what I tried initially and it caused random crashes in CPAchecker due to the duplicate class issue (see the top of this thread here). As we need CPAchecker to work on benchcloud this seemed like a show stopper to me.

What does the BenchCloud have to do with this?

Of course we want CPAchecker to work, and if there is something easy that the JavaSMT developers could do to make it easier for CPAchecker (or other tools combining JavaSMT and Ultimate), it would be nice if JavaSMT would do so. But I guess CPAchecker is not the only user of JavaSMT and as CPAchecker developers we cannot dictate / block progress of JavaSMT. That would make JavaSMT look like a child project of CPAchecker that is not well suited for other users, and I certainly do not want this!

I guess the main goal of JavaSMT here should be provide the latest version of the solvers, and if there is no reasonable way to make it not conflict with Ultimate, then it is primarily a problem for those who want to combine JavaSMT and Ultimate (i.e., the CPAchecker developers) to solve. My first guess would be that it is hopefully possible for example using different class loaders or shading.

Is there a way to open PRs for the Sosy Ivy repository? It would probably be better to move that discussion somewhere else.

But the discussion about which version of SMTInterpol to use in JavaSMT is obviously best kept in the JavaSMT issue tracker?