diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-02 12:09:10 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-02 12:09:10 -0400 |
commit | a35a8b13924d8f633ced0b72b22cb70b768d530a (patch) | |
tree | 54ae21913161392628c4182960e7cf765f7c4d8e /src/theory/sets | |
parent | 848ca519a29a77fd2f30497845dc0d9e49f55879 (diff) |
fix getModelValue(<non-preregistered term>)
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index d9cc23cbf..60b89451a 100644 --- 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); |