From 5527b0c00639f24b11d5e1d4c69050d908b82400 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 10 Oct 2014 17:16:17 -0400
Subject: [PATCH] Fix issue with shared but non-preregistered term setup.
 Thanks Alvise Rabitti for the report.

---
 src/theory/sets/theory_sets_private.cpp |  3 ++-
 test/regress/regress0/Makefile.am       |  3 ++-
 test/regress/regress0/trim.cvc          | 36 +++++++++++++++++++++++++
 3 files changed, 40 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress0/trim.cvc

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 2035c18b0..cae606409 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -414,6 +414,7 @@ void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
 
 void TheorySetsPrivate::addSharedTerm(TNode n) {
   Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
+  d_termInfoManager->addTerm(n);
   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
 }
 
@@ -513,7 +514,7 @@ bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap,
   BOOST_FOREACH(TNode element, saved) { Debug("sets-model") << element << ", "; }
   Debug("sets-model") << " }" << std::endl;
 
-  if(S.getNumChildren() == 2) {
+  if(theory::kindToTheoryId(S.getKind()) == THEORY_SETS && S.getNumChildren() == 2) {
 
     Elements cur;
 
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 7500186dd..c0ee0f2bb 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -107,7 +107,8 @@ CVC_TESTS = \
 	wiki.21.cvc \
 	simplification_bug3.cvc \
 	queries0.cvc \
-	print_lambda.cvc
+	print_lambda.cvc \
+	trim.cvc
 
 # Regression tests for TPTP inputs
 TPTP_TESTS =
diff --git a/test/regress/regress0/trim.cvc b/test/regress/regress0/trim.cvc
new file mode 100644
index 000000000..8bdbde79a
--- /dev/null
+++ b/test/regress/regress0/trim.cvc
@@ -0,0 +1,36 @@
+% COMMAND-LINE: --finite-model-find
+% EXPECT: sat
+DATATYPE
+	myType = A | B
+END;
+%%% structured datatypes
+myTypeSet: TYPE = SET OF myType;
+myTypeGammaSet: TYPE = [# pos: myTypeSet, neg: myTypeSet #];
+delta: TYPE = ARRAY myType OF myTypeGammaSet;
+labels: TYPE = ARRAY myType OF SET OF STRING;
+
+%%% the empty myTypes set
+emptymyTypeSet : SET OF myType;
+ASSERT emptymyTypeSet = {} :: SET OF myType;
+
+d: delta;
+l: labels;
+
+ASSERT (l[A] = {"L","H"});
+ASSERT (l[B] = {"L"});
+
+ic0_i : myTypeSet;
+ic0_c : myTypeSet;
+ASSERT FORALL (r:myType):
+	(r IS_IN ic0_i) => FORALL (r2: myType): (r2 IS_IN d[r].neg) => r2 IS_IN ic0_c;
+ASSERT {A} <= ic0_i;
+ASSERT ((EXISTS (e0 : myType): (e0 IS_IN ic0_i) => (l[A] <= l[e0]))) OR ((ic0_i & ic0_c) <= emptymyTypeSet);
+
+ic1_i : myTypeSet;
+ic1_c : myTypeSet;
+ASSERT FORALL (r:myType):
+	(r IS_IN d[B].pos) => r IS_IN ic1_i;
+ASSERT ((EXISTS (e1 : myType): (e1 IS_IN ic1_i) => (l[B] <= l[e1]))) OR ((ic1_i & ic1_c) <= emptymyTypeSet);
+
+CHECKSAT;
+%COUNTEREXAMPLE;
-- 
2.30.2