From 290fd9672065cde55b7ed9450af36bec21f08f78 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 29 May 2012 17:56:51 +0000
Subject: [PATCH] Enabled SolveEq bv rewrite

---
 src/theory/bv/theory_bv_rewriter.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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); 
   }
-- 
2.30.2