Error with check() when using FixedPoint

[iGavroche]

Try the following statement in a contract:

const fooFx = fx(1)(Pos, 3);
const barFx = fx(1)(Pos, 2);
const zeroFx = fx(1)(Pos, 0);
check(fooFx + barFx > zeroFx, 'Foo+Bar must be positive');

The compiler returns the following output:

Verifying knowledge assertions
Verifying for generic connector
  Verifying when ALL participants are honest
reachc: The compiler has encountered an internal error:

 Unexpected result from the SMT solver:
  Expected: success
  Result: (error "line 3411 column 32: Sort mismatch at argument #1 for function (declare-fun + (Int Int ) Int ) supplied sort is T12" )


This error indicates a problem with the Reach compiler, not your program. Please report this error, along with the pertinent program, to the Reach team as soon as possible so we can fix it.

Open an issue at: https://github.com/reach-sh/reach-lang/issues

CallStack (from HasCallStack):
  error, called at src/Reach/Util.hs:65:3 in reach-0-t6a9aaBayV7nUd09kpubD:Reach.Util
  impossible, called at src/Reach/Verify/SMT.hs:713:9 in reach-0-t6a9aaBayV7nUd09kpubD:Reach.Verify.SMT

[jeapostrophe]

This was fixed by 27cb964