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

Fatal failure at src/theory/theory_engine.cpp:1167 #5543

Closed
wintered opened this issue Nov 30, 2020 · 0 comments · Fixed by #5579
Closed

Fatal failure at src/theory/theory_engine.cpp:1167 #5543

wintered opened this issue Nov 30, 2020 · 0 comments · Fixed by #5579
Assignees
@ajreynol

Comments

@wintered
Copy link 

[529] % cvc4 --strings-exp -q small.smt2
Fatal failure within CVC4::Node CVC4::TheoryEngine::getModelValue(CVC4::TNode) at src/theory/theory_engine.cpp:1167
Check failure
 d_sharedSolver->isShared(var)
Aborted
[530] % 
[530] % cat small.smt2
(declare-fun a () (Seq (Seq Int)))
(declare-fun b () (Seq (Seq Int)))
(declare-fun c () (Seq (Seq Int)))
(declare-fun d () (Seq (Seq Int)))
(declare-fun e () (Seq Int))
(declare-fun f () (Seq Int))
(assert (distinct a (seq.++ (seq.unit e) b)))
(assert (= (seq.++ (seq.unit f) d) a c))
(check-sat)
[531] %

OS: Ubuntu 18.04
Commit: 9f372f0
@ajreynol ajreynol self-assigned this Nov 30, 2020
@ajreynol ajreynol mentioned this issue Dec 2, 2020
Merged
ajreynol added a commit that referenced this issue Dec 8, 2020
@ajreynol
Fix collect model values for sequences of sequences (#5579)
3223d3c 
Fixes #5543.

Recently we changed our model construction for sequences here: #5391.

This fix is not safe for sequences of sequences, where Valuation::getModelValue should not be called, since the argument of the seq.unit is not a shared term.

This makes our model construction for sequences more robust, however I'm not sure this is the end solution. In particular, it is still questionable whether we should call Valuation::getModelValue at all (consider sequences of theories whose model construction comes after strings), or for cases of (seq.unit x) where x is a sequence or string that does not have a concrete value. Regardless, this PR could be merged in the meantime since it should definitely fix some of the current issues.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ajreynol ajreynol

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix collect model values for sequences of sequences ajreynol/CVC4
2 participants
@ajreynol @wintered