Skip to content

Commit 26c14d0

Browse files
author
BaierD
committed
Clean up requireFPToBitvector() implementation
1 parent a4d338f commit 26c14d0

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

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

+3-3
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
package org.sosy_lab.java_smt.test;
1010

1111
import static com.google.common.truth.TruthJUnit.assume;
12+
import static org.sosy_lab.java_smt.api.FormulaType.getSinglePrecisionFloatingPointType;
1213
import static org.sosy_lab.java_smt.test.BooleanFormulaSubject.assertUsing;
1314
import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
1415

@@ -39,7 +40,6 @@
3940
import org.sosy_lab.java_smt.api.FloatingPointFormulaManager;
4041
import org.sosy_lab.java_smt.api.Formula;
4142
import org.sosy_lab.java_smt.api.FormulaManager;
42-
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
4343
import org.sosy_lab.java_smt.api.IntegerFormulaManager;
4444
import org.sosy_lab.java_smt.api.Model;
4545
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
@@ -241,11 +241,11 @@ protected final void requireBitvectorToInt() {
241241
.isNotEqualTo(Solvers.YICES2);
242242
}
243243

244+
@SuppressWarnings("CheckReturnValue")
244245
protected final void requireFPToBitvector() {
245246
requireFloats();
246247
try {
247-
fpmgr.toIeeeBitvector(
248-
fpmgr.makeNumber(0, FloatingPointType.getSinglePrecisionFloatingPointType()));
248+
fpmgr.toIeeeBitvector(fpmgr.makeNumber(0, getSinglePrecisionFloatingPointType()));
249249
} catch (UnsupportedOperationException e) {
250250
assume()
251251
.withMessage("Solver %s does not yet support FP-to-BV conversion", solverToUse())

0 commit comments

Comments
 (0)