diff options
| author | Morgan Deters <mdeters@morgandeters.com> | 2014-10-02 13:10:51 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@morgandeters.com> | 2014-10-02 13:10:51 -0400 |
| commit | 7388ddece082dc254f4b04ce5109427cd340fde4 (patch) | |
| tree | 54ae21913161392628c4182960e7cf765f7c4d8e | |
| parent | 848ca519a29a77fd2f30497845dc0d9e49f55879 (diff) | |
| parent | a35a8b13924d8f633ced0b72b22cb70b768d530a (diff) | |
Merge pull request #54 from kbansal/bugfix_setssegfault
fix getModelValue(<non-preregistered term>)
| -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); |