Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Soundness bug in QF_UFLIA #2835

Closed
numairmansur opened this issue Dec 31, 2019 · 3 comments
Closed

Soundness bug in QF_UFLIA #2835

numairmansur opened this issue Dec 31, 2019 · 3 comments
Assignees
@levnach

Comments

@numairmansur
Copy link

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

qf_uflia.smt2.zip

$ z3 qf_uflia.smt2
sat
sat
unsat

CVC4 return:
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"

$ git log -1
commit 1fff7bb
Author: Lev Nachmanson [email protected]
Date: Mon Dec 30 17:58:56 2019 -0800
use u_map in lar_term
Signed-off-by: Lev Nachmanson [email protected]
@NikolajBjorner
Copy link
Contributor

C:\z3\build>z3 ufl\qf_uflia.smt2
sat
sat
ASSERTION VIOLATION
File: ..\src\util\lp\lar_solver.cpp
Line: 860
(m_settings.random_next() % 100) != 0 || m_status != lp_status::OPTIMAL || all_constraints_hold()

@NikolajBjorner
Copy link
Contributor

@levnach

@levnach
Copy link
Contributor

levnach commented Jan 21, 2020 •
edited
Loading

It seems fixed now.

@levnach levnach closed this as completed Jan 24, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@levnach levnach

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@NikolajBjorner @numairmansur @levnach