Re-enable Z3 4.5.0 for better interpolation #536

leventeBajczi · 2025-10-17T08:47:07Z

Old versions of z3 were really good at interpolation, and I want to add support for it in JavaSMT.

To this end, I've added the implementation of a Z3Legacy solver (to be renamed, as discussed with @baierd), which builds on the 4.5.0 release of z3, rebuilt to use com.microsoft.z3legacy as its package name to avoid name collisions with new z3.

Pre-built binaries with the modifications are available at https://github.com/leventeBajczi/z3/releases/tag/legacy-4.3.0-15644597379, which Theta already uses like this. This should be somehow integrated into the solver management of JavaSMT, which I have no experience with.

To demonstrate how good this version of Z3 is, I ran some preliminary tests in CPAchecker, and found that an NLA encoding of programs using Z3 as the interpolation solver in the predicate analysis configuration results in 510 successfully solved tasks, which are otherwise unsolved by the bitprecise encoding of the same tasks with mathsat5.

Also, I found that #381 (which I opened) is referenced in 3 of the tests, that now failed on this implementation. I removed the overly constraining line which expected the constraint IDs to be unique, which is not necessary IMO if the interpolation problem reported in that issue is otherwise handled - which it seems to be.

baierd · 2025-10-29T11:44:25Z

Thank you very much for the PR! It seems like the old Z3 version is beneficial to have. Could you also post the tables and/or quantile-plots from your experiments (for documentation purposes)?

We need to make sure that there are no issues when running both Z3 instances at the same time! I'll try to start some tests in CPAchecker and report back.

leventeBajczi · 2025-10-30T10:50:02Z

Sure! Here are some:
z3-vs-baseline.table.html
In particular, the #/table?filter=0(0*status*(status(notIn()),category(in(correct)))),1(0*status*(status(notIn()),category(in(error)))) filter shows the real advantage of using Z3 with nonlinear integers complementing the best bitvector config (can solve 510 unsolved tasks).

baierd · 2025-10-31T10:18:11Z

Thank you very much!

Btw. could you try using Z3 version 4.5 from our Ivy repo?
Maybe the old lib still works?

leventeBajczi · 2025-10-31T12:47:04Z

I haven't used it, but I'd be cautious about using it. The libraries I built use the com.microsoft.z3legacy package, as to not mistakenly use a mismatched java/native library.

baierd · 2025-10-31T19:05:56Z

I haven't used it, but I'd be cautious about using it. The libraries I built use the com.microsoft.z3legacy package, as to not mistakenly use a mismatched java/native library.

Good to know! So we need to compile and release it again. Thanks for the clarification!

leventeBajczi · 2025-10-31T19:08:30Z

Well, I'd suggest just using the ones I linked to, but sure, I can also provide a patch on top of the 4.5.0 Z3 so that you can rebuild it if you'd prefer.

baierd

I can't find more issues than some small suggestions and quantifier visitation being outdated. Good job and thank you for all your work!

I suggest to import this into a branch in JavaSMT first, then add the binaries to Ivy, run a more complex test-setup in CPAchecker before merging.

baierd · 2025-10-31T19:06:35Z

src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java

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


Nice catch, fixed!

baierd · 2025-10-31T19:07:57Z

src/org/sosy_lab/java_smt/SolverContextFactory.java

    MATHSAT5,
    SMTINTERPOL,
    Z3,
+    Z3LEGACY,


@kfriedberger @PhilippWendler @leventeBajczi i kinda feel like Z3 legacy is a little unspecific. Since the version is fixed, should we use the actual version? I.e. Z3-3.5?

The solver is able to provide its version string anyway. As it is a version of Z3 with interpolation support, we might name it Z3_INTERPOLATION or simply Z3_3_5 . Special chars like dots or hyphens are not allowed in Java enums.

The JavaSMT enum it independent of the native library, so the library can be called z3Legacy or similar.

I like encoding the version (Z3_INTERPOLATION could I think be confused with iZ3), so I changed it to Z3_4_5_0.

baierd · 2025-10-31T19:22:35Z

src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java

+      storedConstraints = new ArrayDeque<>();
+      storedConstraints.push(PathCopyingPersistentTreeMap.of());
+    } else {
+      storedConstraints = null; // we use NULL as flag for "no unsat-core"


Using Optional would reduce the chance of accidental null access.

We could go through the whole code once and update to latest coding conventions, and include latest bugfixes from Z3.

... i mean, including latest bugfixes for JavaSMT only, no bugfixes for an outdated Z3. 😄

I agree. This should include Z3 as well, since this for example is still present in our Z3. But this should be done independently of Levis work and help, as he/we want this for SVCOMP this year actually ;D

I fixed it in this file; but this came directly from the Z3 implementation, and I did not touch that now. I agree this should probably be fixed globally in the project.

baierd · 2025-10-31T19:30:13Z

src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java

+                Native.getAppDecl(environment, f)));
+      case Z3_VAR_AST:
+        int deBruijnIdx = Native.getIndexValue(environment, f);
+        return visitor.visitBoundVariable(formula, deBruijnIdx);


Please note that visitBoundVariable() has recently been deprecated.
visitQuantifier() now returns the free variable equivalents for all bound variables and the body with all the bound variables re-substituted.

I think this should probably be fixed together with the up-to-date z3 formula creator, and I'd prefer to leave this part as close in the two implementations as possible. LMK if you don't agree!

baierd · 2025-11-01T13:42:41Z

Well, I'd suggest just using the ones I linked to, but sure, I can also provide a patch on top of the 4.5.0 Z3 so that you can rebuild it if you'd prefer.

We want to use a uniform build-process and build-system, as the dependencies used when building may depend on the system used. Also, the scripts do everything more or less automatically anyway, including the upload. @kfriedberger knows more about the publishing, but it might be more work to re-use your binaries compared to executing a command.

You have to remember that even for a fixed Z3 version, the libraries behind it might be updated from time to time!

leventeBajczi · 2025-11-01T14:07:15Z

Thanks for the reviews and the answers! I'll get to fixing the code soon, but in the meantime, I prepared a patch:
z3legacy.patch
This can be applied to the 4.5.0 tag and then built with

mkdir release
python2.7 scripts/mk_make.py --prefix=$PWD/release --java
cd build/ && make -j $(nproc) && make install

(i.e., the usual build command back in 4.5.0 times 😅 )

Besides the package rename, this also fixes some weird issue in the hwf.cpp file. I just took a later version's equivalent code, and for us, this has been working for the past ~1 year, so I think it's safe to say it didn't break something trivial, and fixed that weird behavior.

leventeBajczi added 4 commits October 16, 2025 10:56

Added z3legacy implementation

8874ec9

Formatted new code

01de644

Re-added mistakenly removed deprecation annotation

afb0445

suppressed warnings

38569fa

baierd requested changes Oct 31, 2025

View reviewed changes

leventeBajczi added 3 commits November 1, 2025 15:33

2024->2025

314229e

Z3_4_5_0 in enum

5c634fa

nullable -> optional

a753732

Re-enable Z3 4.5.0 for better interpolation #536

Are you sure you want to change the base?

Re-enable Z3 4.5.0 for better interpolation #536

Uh oh!

Conversation

leventeBajczi commented Oct 17, 2025

Uh oh!

baierd commented Oct 29, 2025

Uh oh!

leventeBajczi commented Oct 30, 2025

Uh oh!

baierd commented Oct 31, 2025

Uh oh!

leventeBajczi commented Oct 31, 2025

Uh oh!

baierd commented Oct 31, 2025

Uh oh!

leventeBajczi commented Oct 31, 2025

Uh oh!

baierd left a comment

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!

baierd commented Nov 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leventeBajczi commented Nov 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

3 participants

baierd commented Nov 1, 2025 •

edited

Loading

leventeBajczi commented Nov 1, 2025 •

edited

Loading