From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 29 May 2012 17:56:51 +0000 (+0000)
Subject: Enabled SolveEq bv rewrite
X-Git-Tag: cvc5-1.0.0~8137
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=290fd9672065cde55b7ed9450af36bec21f08f78;p=cvc5.git

Enabled SolveEq bv rewrite
---

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index f6bbbd8d1..567f9dc46 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -525,9 +525,9 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) {
     Node resultNode = LinearRewriteStrategy
       < RewriteRule<FailEq>,
         RewriteRule<SimplifyEq>,
-        RewriteRule<ReflexivityEq>
+        RewriteRule<ReflexivityEq>,
         //        ,RewriteRule<BitwiseEq>,
-        //        RewriteRule<SolveEq>
+        RewriteRule<SolveEq>
         >::apply(node);
     return RewriteResponse(REWRITE_DONE, resultNode); 
   }