Fixed test

Author: leventeBajczi

src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java

@@ -8,10 +8,8 @@
 
 package org.sosy_lab.java_smt.solvers.z3;
 
-import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
 import com.microsoft.z3.Native;
-import com.microsoft.z3.Z3Exception;
 import java.math.BigInteger;
 import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
 import org.sosy_lab.java_smt.api.FormulaType;
@@ -75,16 +73,15 @@ protected Long makeNumberImpl(double pN, FloatingPointType pType, Long pRounding
 
   @Override
   protected Long makeNumberImpl(
-      BigInteger exponent,
-      BigInteger mantissa,
-      boolean signBit,
-      FloatingPointType type) {
-
-    long signBv = Native.mkBvNumeral(z3context, 1, new boolean[]{signBit});
-    long expoBv = Native.mkNumeral(z3context, exponent.toString(), Native.mkBvSort(z3context,
-        type.getExponentSize()));
-    long mantBv = Native.mkNumeral(z3context, mantissa.toString(), Native.mkBvSort(z3context,
-        type.getMantissaSize()));
+      BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
+
+    long signBv = Native.mkBvNumeral(z3context, 1, new boolean[] {signBit});
+    long expoBv =
+        Native.mkNumeral(
+            z3context, exponent.toString(), Native.mkBvSort(z3context, type.getExponentSize()));
+    long mantBv =
+        Native.mkNumeral(
+            z3context, mantissa.toString(), Native.mkBvSort(z3context, type.getMantissaSize()));
 
     assert Native.getSort(z3context, signBv) != Native.getSort(z3context, mantBv);
 

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

@@ -953,10 +953,10 @@ public void failOnInvalidString() {
 
   @Test
   public void fpFromBitPattern() throws SolverException, InterruptedException {
-    final FloatingPointFormula expr1 = fpmgr.makeNumber(-0.1, doublePrecType);
+    final FloatingPointFormula expr1 = fpmgr.makeNumber(-0.1, singlePrecType);
     final FloatingPointFormula expr2 =
         fpmgr.makeNumber(
-            BigInteger.valueOf(123), BigInteger.valueOf(5033165), true, doublePrecType);
+            BigInteger.valueOf(123), BigInteger.valueOf(5033165), true, singlePrecType);
     assertThatFormula(fpmgr.assignment(expr1, expr2)).isTautological();
   }
 }