projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
848ca51
)
fix getModelValue(<non-preregistered term>)
author
Kshitij Bansal
<kshitij@cs.nyu.edu>
Thu, 2 Oct 2014 16:09:10 +0000
(12:09 -0400)
committer
Kshitij Bansal
<kshitij@cs.nyu.edu>
Thu, 2 Oct 2014 16:09:10 +0000
(12:09 -0400)
src/theory/sets/theory_sets_private.cpp
patch
|
blob
|
history
diff --git
a/src/theory/sets/theory_sets_private.cpp
b/src/theory/sets/theory_sets_private.cpp
index d9cc23cbf78939909fff66a00901f81cc79e6817..60b89451abd795e21850152ac6d0857c62edd2c7 100644
(file)
--- a/
src/theory/sets/theory_sets_private.cpp
+++ b/
src/theory/sets/theory_sets_private.cpp
@@
-1437,6
+1437,9
@@
void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n)
{
+ if(d_terms.find(n) == d_terms.end()) {
+ return Node();
+ }
Assert(n.getType().isSet());
set<Node> elements, elements_const;
Node S = d_eqEngine->getRepresentative(n);