Soundness bug in QF_LIA

[numairmansur]

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

qf_lia.smt2.zip

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

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

CVC4 return:

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]

@levnach
C:\z3\build>z3 qf_lia.smt2\qf_lia.smt2
sat
sat
sat
ASSERTION VIOLATION
File: ..\src\util\lp\lar_solver.cpp
Line: 370
ax_is_correct()

[levnach]

The issue does not reproduce anymore.

[NikolajBjorner]

can you backport the fix to master branch?

[levnach]

It does not repro in the Z3Prover repository either.

[NikolajBjorner]

The assertion violation repros beautifully for me

[levnach]

It does not reproduce on Ubuntu, but it does reproduce on Windows...

[levnach]

fixed by removing a wrong assert statement