Switched TheoryModel assertEqualityEngine to use const Equality Engine pointers.

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 882a3034a1f2e2b126e5d17311008e5f65ad6247..2260e86d3a072709e6da033408dc1cddea8b5e02 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -256,7 +256,7 @@ void TheoryModel::assertPredicate( Node a, bool polarity ){
 }
 
 /** assert equality engine */
-void TheoryModel::assertEqualityEngine( eq::EqualityEngine* ee ){
+void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);

diff --git a/src/theory/model.h b/src/theory/model.h
index 940a2f52721d9d5b94ea085f78e6fea18620ebc4..4a4bf48c942d7a2c72fd43a61bddec9cc0f5f679 100644 (file)
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -123,7 +123,7 @@ public:
   /** assert predicate holds in the model */
   void assertPredicate( Node a, bool polarity );
   /** assert all equalities/predicates in equality engine hold in the model */
-  void assertEqualityEngine( eq::EqualityEngine* ee );
+  void assertEqualityEngine( const eq::EqualityEngine* ee );
 public:
   /** general queries */
   bool hasTerm( Node a );