Soundness bug in QF_S in z3-seq

[numairmansur]

Hi,
On the latest nightly build z3-seq gives wrong answer on the following file:

qf_s.smt2.zip

All the formulas at every level in the assertion stack are satisfiable.

$ /z3-nightly/bin/z3 qf_s.smt2
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
unsat

While z3str3 and CVC4 return:

sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat

OS:
NAME="Ubuntu"
VERSION="16.04.5 LTS (Xenial Xerus)"
ID=ubuntu
ID_LIKE=debian
PRETTY_NAME="Ubuntu 16.04.5 LTS"
VERSION_ID="16.04"

[NikolajBjorner]

Fixed, seems #2860 was a duplicate of this