From a35a8b13924d8f633ced0b72b22cb70b768d530a Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 2 Oct 2014 12:09:10 -0400
Subject: [PATCH] fix getModelValue(<non-preregistered term>)

---
 src/theory/sets/theory_sets_private.cpp | 3 +++
 1 file changed, 3 insertions(+)

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);
-- 
2.30.2