BitvectorFormulaManager: improve slow rotation test.

Z3 has a regression since the latest version,
so lets move the boundary lower.

Author: kfriedberger

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);