From c8b948c37364104bf5f9ca5eca83120247b693a4 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 17 Mar 2014 18:01:10 -0400
Subject: [PATCH] Fix for registration issues of term appearing in a shared
 lemma

(brought to attention by lianah -- fix currently just adapted using
arrays -- this is to remind me to raise why do we even have this
isPreregistered bussiness)
---
 src/theory/sets/theory_sets.cpp                |  4 ++++
 src/theory/sets/theory_sets.h                  |  2 ++
 src/theory/sets/theory_sets_private.cpp        | 18 ++++++++++++++++++
 src/theory/sets/theory_sets_private.h          |  2 ++
 .../regress0/sets/sets-testlemma-ints.smt2     |  2 +-
 5 files changed, 27 insertions(+), 1 deletion(-)

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 73176ff8b..3a5b61390 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -34,6 +34,10 @@ TheorySets::~TheorySets() {
   delete d_internal;
 }
 
+void TheorySets::addSharedTerm(TNode n) {
+  d_internal->addSharedTerm(n);
+}
+
 void TheorySets::check(Effort e) {
   d_internal->check(e);
 }
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 8900b0e38..f40031514 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -46,6 +46,8 @@ public:
 
   ~TheorySets();
 
+  void addSharedTerm(TNode);
+
   void check(Effort);
 
   void collectModelInfo(TheoryModel*, bool fullModel);
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 17eaf80aa..b45874bf2 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -54,6 +54,19 @@ void TheorySetsPrivate::check(Theory::Effort level) {
     bool polarity = fact.getKind() != kind::NOT;
     TNode atom = polarity ? fact : fact[0];
 
+    if (!assertion.isPreregistered) {
+      if (atom.getKind() == kind::EQUAL) {
+        if (!d_equalityEngine.hasTerm(atom[0])) {
+          Assert(atom[0].isConst());
+          d_equalityEngine.addTerm(atom[0]);
+        }
+        if (!d_equalityEngine.hasTerm(atom[1])) {
+          Assert(atom[1].isConst());
+          d_equalityEngine.addTerm(atom[1]);
+        }
+      }
+    }
+
     // Solve each
     switch(atom.getKind()) {
     case kind::EQUAL:
@@ -710,6 +723,11 @@ bool TheorySetsPrivate::propagate(TNode literal) {
 }/* TheorySetsPropagate::propagate(TNode) */
 
 
+void TheorySetsPrivate::addSharedTerm(TNode n) {
+  Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
+  d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
+}
+
 void TheorySetsPrivate::conflict(TNode a, TNode b)
 {
   if (a.getKind() == kind::CONST_BOOLEAN) {
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 1f43ede42..58000e435 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -47,6 +47,8 @@ public:
 
   ~TheorySetsPrivate();
 
+  void addSharedTerm(TNode);
+
   void check(Theory::Effort);
 
   void collectModelInfo(TheoryModel*, bool fullModel);
diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2
index c8277be71..9dd257401 100644
--- a/test/regress/regress0/sets/sets-testlemma-ints.smt2
+++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2
@@ -3,5 +3,5 @@
 (set-info :status sat)
 (declare-fun x () (Set Int))
 (declare-fun y () (Set Int))
-(assert (= x y))
+(assert (not (= x y)))
 (check-sat)
-- 
2.30.2