From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 17 Aug 2021 14:45:23 +0000 (-0500)
Subject: Make theory BV use central eq engine when option is enabled (#7025)
X-Git-Tag: cvc5-1.0.0~1378
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d39e1b906b47ef8e953dac297fa0fb565dd040a4;p=cvc5.git

Make theory BV use central eq engine when option is enabled (#7025)
---

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index b774d456a..04bab16e2 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -620,7 +620,7 @@ bool Theory::usesCentralEqualityEngine(TheoryId id)
   }
   return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS
          || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS
-         || id == THEORY_SEP || id == THEORY_ARRAYS;
+         || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV;
 }
 
 bool Theory::expUsingCentralEqualityEngine(TheoryId id)