Z3: revert 19d8e34 where we limited the tests of Z3 to a smaller test input

Author: kfriedberger

src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java

@@ -468,9 +468,6 @@ public void bvRotateByBV() throws SolverException, InterruptedException {
       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;