Skip to content

Commit 35b9b34

Browse files
committed
reduce some tests that are quite similar.
1 parent 7b01966 commit 35b9b34

File tree

2 files changed

+6
-6
lines changed

2 files changed

+6
-6
lines changed

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ public class FloatingPointFormulaManagerTest
4747
// numbers are small enough to be precise with single precision
4848
private static final int[] SINGLE_PREC_INTS = new int[] {0, 1, 2, 5, 10, 20, 50, 100, 200, 500};
4949

50-
private static final int NUM_RANDOM_TESTS = 100;
50+
private static final int NUM_RANDOM_TESTS = 50;
5151

5252
private FloatingPointType singlePrecType;
5353
private FloatingPointType doublePrecType;
@@ -867,8 +867,8 @@ private List<Float> getListOfFloats() {
867867
flts.add(-0.0f); // MathSat5 fails for NEGATIVE_ZERO
868868
}
869869

870-
for (int i = 1; i < 20; i++) {
871-
for (int j = 1; j < 20; j++) {
870+
for (int i = 1; i < 10; i++) {
871+
for (int j = 1; j < 10; j++) {
872872
flts.add((float) (i * Math.pow(10, j)));
873873
flts.add((float) (-i * Math.pow(10, j)));
874874
}
@@ -904,8 +904,8 @@ private List<Double> getListOfDoubles() {
904904
dbls.add(-0.0); // MathSat5 fails for NEGATIVE_ZERO
905905
}
906906

907-
for (int i = 1; i < 20; i++) {
908-
for (int j = 1; j < 20; j++) {
907+
for (int i = 1; i < 10; i++) {
908+
for (int j = 1; j < 10; j++) {
909909
dbls.add(i * Math.pow(10, j));
910910
dbls.add(-i * Math.pow(10, j));
911911
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ public class ModelEvaluationTest extends SolverBasedTest0.ParameterizedSolverBas
5151

5252
@Override
5353
protected ConfigurationBuilder createTestConfigBuilder() {
54-
problemSize = solverToUse() == Solvers.PRINCESS ? 10 : 100; // Princess is too slow.
54+
problemSize = solverToUse() == Solvers.PRINCESS ? 10 : 50; // Princess is too slow.
5555
ConfigurationBuilder builder = super.createTestConfigBuilder();
5656
if (solverToUse() == Solvers.MATHSAT5) {
5757
builder.setOption("solver.mathsat5.furtherOptions", "model_generation=true");

0 commit comments

Comments
 (0)