Skip to content

Commit 4bf4133

Browse files
committed
fixed a crucial implementation mistake, where all numbers were handed to Floating-Points as Strings
1 parent 6b18557 commit 4bf4133

File tree

1 file changed

+6
-6
lines changed

1 file changed

+6
-6
lines changed

src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java

+6-6
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ public FloatingPointFormula makeNumber(Rational pN, FormulaType.FloatingPointTyp
6767
wrap(makeNumberImpl(pN.toString(), pType, getDefaultRoundingMode()));
6868
if (Generator.isLoggingEnabled()) {
6969
FloatingPointGenerator.logMakeFloatingPoint(
70-
result, pType.getExponentSize(), pType.getMantissaSize(), pN.toString());
70+
result, pType.getExponentSize(), pType.getMantissaSize(), pN);
7171
}
7272
return result;
7373
}
@@ -79,7 +79,7 @@ public FloatingPointFormula makeNumber(
7979
wrap(makeNumberImpl(pN.toString(), pType, getRoundingMode(pRoundingMode)));
8080
if (Generator.isLoggingEnabled()) {
8181
FloatingPointGenerator.logMakeFloatingPoint(
82-
result, pType.getExponentSize(), pType.getMantissaSize(), pN.toString());
82+
result, pType.getExponentSize(), pType.getMantissaSize(), pN);
8383
}
8484
return result;
8585
}
@@ -89,7 +89,7 @@ public FloatingPointFormula makeNumber(double pN, FormulaType.FloatingPointType
8989
FloatingPointFormula result = wrap(makeNumberImpl(pN, pType, getDefaultRoundingMode()));
9090
if (Generator.isLoggingEnabled()) {
9191
FloatingPointGenerator.logMakeFloatingPoint(
92-
result, pType.getExponentSize(), pType.getMantissaSize(), String.valueOf(pN));
92+
result, pType.getExponentSize(), pType.getMantissaSize(), pN);
9393
}
9494
return result;
9595
}
@@ -100,7 +100,7 @@ public FloatingPointFormula makeNumber(
100100
FloatingPointFormula result = wrap(makeNumberImpl(pN, pType, getRoundingMode(pRoundingMode)));
101101
if (Generator.isLoggingEnabled()) {
102102
FloatingPointGenerator.logMakeFloatingPoint(
103-
result, pType.getExponentSize(), pType.getMantissaSize(), String.valueOf(pN));
103+
result, pType.getExponentSize(), pType.getMantissaSize(), pN);
104104
}
105105
return result;
106106
}
@@ -113,7 +113,7 @@ public FloatingPointFormula makeNumber(BigDecimal pN, FormulaType.FloatingPointT
113113
FloatingPointFormula result = wrap(makeNumberImpl(pN, pType, getDefaultRoundingMode()));
114114
if (Generator.isLoggingEnabled()) {
115115
FloatingPointGenerator.logMakeFloatingPoint(
116-
result, pType.getExponentSize(), pType.getMantissaSize(), String.valueOf(pN));
116+
result, pType.getExponentSize(), pType.getMantissaSize(), pN);
117117
}
118118
return result;
119119
}
@@ -124,7 +124,7 @@ public FloatingPointFormula makeNumber(
124124
FloatingPointFormula result = wrap(makeNumberImpl(pN, pType, getRoundingMode(pRoundingMode)));
125125
if (Generator.isLoggingEnabled()) {
126126
FloatingPointGenerator.logMakeFloatingPoint(
127-
result, pType.getExponentSize(), pType.getMantissaSize(), String.valueOf(pN));
127+
result, pType.getExponentSize(), pType.getMantissaSize(), pN);
128128
}
129129
return result;
130130
}

0 commit comments

Comments
 (0)