Fix for model building with shared terms for arithmetic.

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 7 insertions, 0 deletions

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index cdad1e19c..43574f6e4 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -237,6 +237,13 @@ int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) {
 //  }
 //}
 
+std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
+  std::hash_set<TNode, TNodeHashFunction> currentlyShared;
+  for(shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i){
+    currentlyShared.insert (*i);
+  }
+  return currentlyShared;
+}
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */