TS Add operation is not solved into path constraints properly

[zishkaz]

Bug Description

Consider this test (remake of argWithArg from resources/samples/TypeCoercion.ts):

plus(a: number, b: number): number {
      if (a + b == 10.0) {
          return 1
      } else {
          return 0
      }
}

In current state, USVM TS for path that retuns 1 will return a model containing a and b, sum of which is not 10.0. This model contradicts path constraints.

Extracted values:
	[Double(value=10.0), Double(value=2.578975581576977E-231), Double(value=1.0)] // false model, 10.0 + 2.57 != 10.0
	[Double(value=0.0), Double(value=0.0), Double(value=0.0)]

Nevertheless, correct SAT-solver expression is generated for condition a + b == 10.0:
KEqExpr(KFpAddExpr(a, b), KFp64(10.0)))

Research

Functional comparison with USVM Java is difficult because the same function plus above written in Java won't produce equality operation in if statement. Instead, it will use JacoDB jvm-specific Cmpl operator in three-address code. Cmpl has different semantics from true/false equality and does not have any alternatives in TypeScript three-address code.

USVM TS machine code examination didn't yield any results since generated path constraints are correct.

Possible USVM core error, or complex symbolic expressions' misuse.