merged dejan's stuff

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index f1255e07c82d8db5ed290e06630f1931c8809e36..d8fc596c0b9f0aadd75310f3cd8f542d98cc51d5 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -39,7 +39,7 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
   if (d_useEqualityEngine) {
 
     // The kinds we are treating as function application in congruence
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
@@ -48,8 +48,8 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT);
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
     d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);