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

CVC4 crashes with --check-unsat-cores #3474

Closed
wintered opened this issue Nov 18, 2019 · 1 comment
Closed

CVC4 crashes with --check-unsat-cores #3474

wintered opened this issue Nov 18, 2019 · 1 comment
Assignees

Comments

@wintered
Copy link

Hi,

CVC4 with --check-unsat-cores option crashes on the following formula

(set-logic ALL)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (= b 0))
(assert (or (= a 6) (= a 9)))
(assert (> (- c b) 11))
(assert (not (= 0 (- c a) 3)))
(assert (or (= a 0) (= (- a c) 1)))
(assert (or (> (- c a) 2) (<= (- c a) 3)))
Fatal failure within void CVC4::ProofManager::traceDeps(CVC4::TNode, CVC4::CDExprSet*) at /home/suz/software/CVC4/src/proof/proof_manager.cpp:317
Internal error detectedCannot trace dependence information back to input assertion:
`(let ((_let_0 (+ (- 3) c))) (or (<= a _let_0) (>= a _let_0)))'
Aborted

OS: Ubuntu 18.04
Revision: 11bc0e4

@4tXJ7f 4tXJ7f self-assigned this Nov 18, 2019
@nafur
Copy link
Member

nafur commented Sep 3, 2020

This issue has been resolved with b90cfb4. I thus close this issue.

@nafur nafur closed this as completed Sep 3, 2020
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