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.

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

Invalid model for QF_AUFBV formula #5743

Closed
rainoftime opened this issue Jan 5, 2021 · 1 comment
Closed

Invalid model for QF_AUFBV formula #5743

rainoftime opened this issue Jan 5, 2021 · 1 comment
Assignees

Comments

@rainoftime
Copy link

rainoftime commented Jan 5, 2021

Hi, for the following formula,
CVC e0dfc0a

(set-logic QF_AUFBV)
(declare-fun bv_22-0 () (_ BitVec 1))
(declare-fun arr-8324605531633220487_-1461211092162269148-0 () (Array (_ BitVec 1) Bool))
(assert (select arr-8324605531633220487_-1461211092162269148-0 (bvlshr bv_22-0 bv_22-0)))
(check-sat)

$ cvc -q --check-models delta.out.smt2 
Fatal failure within void CVC4::smt::CheckModels::checkModel(CVC4::smt::Model*, CVC4::context::CDList<CVC4::NodeTemplate<true> >*, bool) at /CV4/src/smt/check_models.cpp:129
Internal error detectedSmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:
assertion:     (select arr-8324605531633220487_-1461211092162269148-0 (bvlshr bv_22-0 bv_22-0))
simplifies to: false
expected `true'.
Run with `--check-models -v' for additional diagnostics.
Aborted
ajreynol pushed a commit that referenced this issue Jun 4, 2021
This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.

Fixes #3958, #5396, #5736, #5743, #5947.
@mpreiner
Copy link
Member

mpreiner commented Jun 4, 2021

Fixed by #6660.

@mpreiner mpreiner closed this as completed Jun 4, 2021
4tXJ7f pushed a commit that referenced this issue Jun 8, 2021
This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.

Fixes #3958, #5396, #5736, #5743, #5947.
4tXJ7f pushed a commit to 4tXJ7f/cvc5 that referenced this issue Jun 11, 2021
This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.

Fixes cvc5#3958, cvc5#5396, cvc5#5736, cvc5#5743, cvc5#5947.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants