diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2013-03-19 22:25:40 -0400 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2013-03-19 22:25:40 -0400 |
| commit | 170d322c39a72cb48dc892e71176862c473ae75b (patch) | |
| tree | 40f4a1475375f37f957e1e6750af089979f11bb5 /src/theory | |
| parent | c30b3e2c03f9c3df51eb8d2e7cb6c72907cb77c0 (diff) | |
merged dejan's stuff
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
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); |