fix getModelValue(<non-preregistered term>)
authorKshitij Bansal <kshitij@cs.nyu.edu>
Thu, 2 Oct 2014 16:09:10 +0000 (12:09 -0400)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Thu, 2 Oct 2014 16:09:10 +0000 (12:09 -0400)
src/theory/sets/theory_sets_private.cpp

index d9cc23cbf78939909fff66a00901f81cc79e6817..60b89451abd795e21850152ac6d0857c62edd2c7 100644 (file)
@@ -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);