From: Liana Hadarean <lianahady@gmail.com>
Date: Wed, 20 Mar 2013 02:25:40 +0000 (-0400)
Subject: merged dejan's stuff
X-Git-Tag: cvc5-1.0.0~7361^2~35
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=170d322c39a72cb48dc892e71176862c473ae75b;p=cvc5.git

merged dejan's stuff
---

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index f1255e07c..d8fc596c0 100644
--- 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);