Soundness bug in QF_FP

[numairmansur]

Hi,
z3 gives wrong answer on the following file:

qf_fp.smt2

All the formulas at every level in the assertion stack are satisfiable, but z3 returns:

sat
unsat

While CVC4 return:

sat
sat

OS:
NAME="Ubuntu"
VERSION="16.04.5 LTS (Xenial Xerus)"

commit: 3dc822c

[wintersteiger]

Likely a duplicate of #2827 (in progress).

[numairmansur]

This seems fixed in the latest release @NikolajBjorner

[wintersteiger]

After additional checks, I can confirm this is fixed.