Skip to content

Commit 050931e

Browse files
committed
code style: JavaSMT is not yet ready for the latest Java features.
1 parent 19d8e34 commit 050931e

File tree

1 file changed

+12
-6
lines changed

1 file changed

+12
-6
lines changed

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

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -463,12 +463,18 @@ public void bvRotateByConstant() throws SolverException, InterruptedException {
463463

464464
@Test
465465
public void bvRotateByBV() throws SolverException, InterruptedException {
466-
int[] bitsizes =
467-
switch (solverToUse()) {
468-
case PRINCESS -> new int[] {2, 3}; // Princess is too slow for larger bitvectors
469-
case Z3 -> new int[] {2, 3, 4, 8}; // Z3 is too slow for larger bitvectors since v4.15.0
470-
default -> new int[] {2, 3, 4, 8, 13, 25, 31};
471-
};
466+
int[] bitsizes;
467+
switch (solverToUse()) {
468+
case PRINCESS:
469+
bitsizes = new int[] {2, 3}; // Princess is too slow for larger bitvectors
470+
break;
471+
case Z3:
472+
bitsizes = new int[] {2, 3, 4, 8}; // Z3 is too slow for larger bitvectors since v4.15.0
473+
break;
474+
default:
475+
bitsizes = new int[] {2, 3, 4, 8, 13, 25, 31};
476+
break;
477+
}
472478

473479
for (int bitsize : bitsizes) {
474480
BitvectorFormula zero = bvmgr.makeBitvector(bitsize, 0);

0 commit comments

Comments
 (0)