From 9dc75785d263450c5aed4e03e3b34cfa047ed3f9 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 27 Jul 2025 11:57:05 +0200 Subject: [PATCH 1/8] Z3: update from version 4.14.0. to 4.14.1 --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 5bf392b47c..eb2fecb5d6 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -189,7 +189,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 7519d614c7167c870dacbe8ea989deb287a9a90c Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 27 Jul 2025 12:05:57 +0200 Subject: [PATCH 2/8] Z3: update from version 4.14.1 to 4.15.0 --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index eb2fecb5d6..cd6a465223 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -189,7 +189,7 @@ SPDX-License-Identifier: Apache-2.0 - + From afd4fef4053c7c04d7866711cc2610b7d98c82fa Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 27 Jul 2025 12:12:25 +0200 Subject: [PATCH 3/8] Z3: update from version 4.15.0 to 4.15.1 --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index cd6a465223..20f2fe9e19 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -189,7 +189,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 937dbb98d9d802ee0445d173750aa30e86c44629 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 27 Jul 2025 12:18:06 +0200 Subject: [PATCH 4/8] Z3: update from version 4.15.1 to 4.15.2 --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 20f2fe9e19..0e94f6096b 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -189,7 +189,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 2cb409a9539740a2669cee910ee3b744a6191b87 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 27 Jul 2025 15:36:00 +0200 Subject: [PATCH 5/8] BitvectorFormulaManager: fix ROL/ROR for cases, where rotation is done by bitsize^2-1. The bug should when using small bitsize (=2) and rotate by 1. --- .../java_smt/basicimpl/AbstractBitvectorFormulaManager.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java index 19a797a485..46455c4829 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java @@ -340,7 +340,7 @@ public BitvectorFormula rotateLeft(BitvectorFormula pNumber, BitvectorFormula pT protected TFormulaInfo rotateLeft(TFormulaInfo pNumber, TFormulaInfo pToRotate) { int length = getLength(wrap(pNumber)); final TFormulaInfo lengthAsBv = makeBitvectorImpl(length, length); - final TFormulaInfo toRotateInRange = smodulo(pToRotate, lengthAsBv); + final TFormulaInfo toRotateInRange = remainder(pToRotate, lengthAsBv, false); return or( shiftLeft(pNumber, toRotateInRange), shiftRight(pNumber, subtract(lengthAsBv, toRotateInRange), false)); @@ -373,7 +373,7 @@ public BitvectorFormula rotateRight(BitvectorFormula pNumber, BitvectorFormula p protected TFormulaInfo rotateRight(TFormulaInfo pNumber, TFormulaInfo pToRotate) { int length = getLength(wrap(pNumber)); final TFormulaInfo lengthAsBv = makeBitvectorImpl(length, length); - final TFormulaInfo toRotateInRange = smodulo(pToRotate, lengthAsBv); + final TFormulaInfo toRotateInRange = remainder(pToRotate, lengthAsBv, false); return or( shiftRight(pNumber, toRotateInRange, false), shiftLeft(pNumber, subtract(lengthAsBv, toRotateInRange))); From 19d8e343de70dc212e1dacbb08e1ed88307b6179 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 27 Jul 2025 15:37:06 +0200 Subject: [PATCH 6/8] BitvectorFormulaManager: improve slow rotation test. Z3 has a regression since the latest version, so lets move the boundary lower. --- .../test/BitvectorFormulaManagerTest.java | 24 ++++++++++++++----- 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java index 59cd0c3d92..dd91346018 100644 --- a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java @@ -463,12 +463,14 @@ public void bvRotateByConstant() throws SolverException, InterruptedException { @Test public void bvRotateByBV() throws SolverException, InterruptedException { - assume() - .withMessage("Princess is too slow for this test") - .that(solver) - .isNotEqualTo(Solvers.PRINCESS); - - for (int bitsize : new int[] {8, 13, 25, 31}) { + int[] bitsizes = + switch (solverToUse()) { + case PRINCESS -> new int[] {2, 3}; // Princess is too slow for larger bitvectors + case Z3 -> new int[] {2, 3, 4, 8}; // Z3 is too slow for larger bitvectors since v4.15.0 + default -> new int[] {2, 3, 4, 8, 13, 25, 31}; + }; + + for (int bitsize : bitsizes) { BitvectorFormula zero = bvmgr.makeBitvector(bitsize, 0); BitvectorFormula a = bvmgr.makeVariable(bitsize, "a" + bitsize); BitvectorFormula b = bvmgr.makeVariable(bitsize, "b" + bitsize); @@ -600,6 +602,16 @@ public void bvModulo() throws SolverException, InterruptedException { assertThatFormula(bvmgr.equal(bvmgr.smodulo(minusTen, minusThree), minusOne)).isTautological(); } + @Test + public void bvModulo2() throws SolverException, InterruptedException { + BitvectorFormula one = bvmgr.makeBitvector(2, 1); + BitvectorFormula two = bvmgr.makeBitvector(2, 2); + BitvectorFormula three = bvmgr.makeBitvector(2, 3); + + // check that SMOD works for small bitvectors: 1_2 % 2_2 == 3_2 or 01 % 10 == 11 + assertThatFormula(bvmgr.equal(bvmgr.smodulo(one, two), three)).isTautological(); + } + @Test public void bvModuloByZero() throws SolverException, InterruptedException { BitvectorFormula ten = bvmgr.makeBitvector(8, 10); From 050931e106b1fb10b94b34a4e47f414602229921 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 27 Jul 2025 15:52:33 +0200 Subject: [PATCH 7/8] code style: JavaSMT is not yet ready for the latest Java features. --- .../test/BitvectorFormulaManagerTest.java | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java index dd91346018..84888140af 100644 --- a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java @@ -463,12 +463,18 @@ public void bvRotateByConstant() throws SolverException, InterruptedException { @Test public void bvRotateByBV() throws SolverException, InterruptedException { - int[] bitsizes = - switch (solverToUse()) { - case PRINCESS -> new int[] {2, 3}; // Princess is too slow for larger bitvectors - case Z3 -> new int[] {2, 3, 4, 8}; // Z3 is too slow for larger bitvectors since v4.15.0 - default -> new int[] {2, 3, 4, 8, 13, 25, 31}; - }; + int[] bitsizes; + switch (solverToUse()) { + case PRINCESS: + bitsizes = new int[] {2, 3}; // Princess is too slow for larger bitvectors + break; + case Z3: + bitsizes = new int[] {2, 3, 4, 8}; // Z3 is too slow for larger bitvectors since v4.15.0 + break; + default: + bitsizes = new int[] {2, 3, 4, 8, 13, 25, 31}; + break; + } for (int bitsize : bitsizes) { BitvectorFormula zero = bvmgr.makeBitvector(bitsize, 0); From 4070cfc1bac8973340de3e3f8bb2c42d74de95f1 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 27 Jul 2025 19:40:48 +0200 Subject: [PATCH 8/8] fix tests for BV-rotation --- .../java_smt/test/RotationVisitorTest.java | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/RotationVisitorTest.java b/src/org/sosy_lab/java_smt/test/RotationVisitorTest.java index be5b410894..d215e3df7c 100644 --- a/src/org/sosy_lab/java_smt/test/RotationVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/RotationVisitorTest.java @@ -51,8 +51,8 @@ public void rotateLeftTest() { FunctionDeclarationKind.ITE, FunctionDeclarationKind.EQ, FunctionDeclarationKind.EQ, - FunctionDeclarationKind.BV_SMOD, - FunctionDeclarationKind.BV_SMOD, + FunctionDeclarationKind.BV_UREM, + FunctionDeclarationKind.BV_UREM, FunctionDeclarationKind.BV_LSHR, FunctionDeclarationKind.BV_SUB); break; @@ -62,8 +62,8 @@ public void rotateLeftTest() { .containsExactly( FunctionDeclarationKind.BV_OR, FunctionDeclarationKind.BV_SHL, - FunctionDeclarationKind.BV_SMOD, - FunctionDeclarationKind.BV_SMOD, + FunctionDeclarationKind.BV_UREM, + FunctionDeclarationKind.BV_UREM, FunctionDeclarationKind.BV_LSHR, FunctionDeclarationKind.BV_SUB); break; @@ -114,8 +114,8 @@ public void rotateRightTest() { FunctionDeclarationKind.ITE, FunctionDeclarationKind.EQ, FunctionDeclarationKind.EQ, - FunctionDeclarationKind.BV_SMOD, - FunctionDeclarationKind.BV_SMOD, + FunctionDeclarationKind.BV_UREM, + FunctionDeclarationKind.BV_UREM, FunctionDeclarationKind.BV_SHL, FunctionDeclarationKind.BV_SUB); break; @@ -125,8 +125,8 @@ public void rotateRightTest() { .containsExactly( FunctionDeclarationKind.BV_OR, FunctionDeclarationKind.BV_SHL, - FunctionDeclarationKind.BV_SMOD, - FunctionDeclarationKind.BV_SMOD, + FunctionDeclarationKind.BV_UREM, + FunctionDeclarationKind.BV_UREM, FunctionDeclarationKind.BV_LSHR, FunctionDeclarationKind.BV_SUB); break;