Skip to content

Commit d72a024

Browse files
committed
- Implemented fp generating correctly and added new tests
1 parent 4451895 commit d72a024

File tree

10 files changed

+676
-570
lines changed

10 files changed

+676
-570
lines changed

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

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -179,13 +179,9 @@ protected TFormulaInfo makeNumberImpl(
179179
public FloatingPointFormula makeNumber(
180180
BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) {
181181
FloatingPointFormula result = wrap(makeNumberImpl(exponent, mantissa, signBit, type));
182-
int sign = signBit ? 1 : 0;
183182
if (Generator.isLoggingEnabled()) {
184-
FloatingPointGenerator.logMakeFloatingPoint(
185-
result,
186-
type.getExponentSize(),
187-
type.getMantissaSize(),
188-
String.valueOf(sign + exponent.intValue() + mantissa.intValue()));
183+
FloatingPointGenerator.logMakeFloatingPointFromBigInteger(
184+
result, exponent, mantissa, signBit, type);
189185
}
190186
return result;
191187
}

0 commit comments

Comments
 (0)