diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-10 17:16:17 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-10 17:16:17 -0400 |
| commit | 5527b0c00639f24b11d5e1d4c69050d908b82400 (patch) | |
| tree | 347f4909159c63daf0c0f5b84ba2a4821db3b069 /src/theory/sets | |
| parent | d9cc527b3edb3ba39f076ce0b77327a473b89b88 (diff) | |
Fix issue with shared but non-preregistered term setup. Thanks Alvise Rabitti for the report.
Diffstat (limited to 'src/theory/sets')
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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; |