From 07c2ba8ec0fba4e63620ea4861a2c79ceb9d8507 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Tue, 30 Apr 2013 15:52:40 -0400
Subject: [PATCH] updated the author name

---
 .../theory_bv_rewrite_rules_normalization.h   |  2 +-
 src/theory/bv/theory_bv_rewriter.cpp          | 20 +++++++++----------
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 035bd4469..2da4dfa6a 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -1120,7 +1120,7 @@ template<> inline
 Node RewriteRule<BitwiseSlicing>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<BitwiseSlicing>(" << node << ")" << std::endl;
   // get the constant
-  bool found_constant = false;
+  bool found_constant CVC4_UNUSED = false ;
   TNode constant;
   std::vector<Node> other_children; 
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 44c498947..0775cb1f8 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -177,10 +177,10 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) {
     return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
   }
 
-  // if (RewriteRule<ExtractSignExtend>::applies(node)) {
-  //   resultNode = RewriteRule<ExtractSignExtend>::run<false>(node);
-  //   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
-  // }
+  if (RewriteRule<ExtractSignExtend>::applies(node)) {
+    resultNode = RewriteRule<ExtractSignExtend>::run<false>(node);
+    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  }
 
   if (RewriteRule<ExtractBitwise>::applies(node)) {
     resultNode = RewriteRule<ExtractBitwise>::run<false>(node);
@@ -228,8 +228,8 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){
   
   resultNode = LinearRewriteStrategy
     < RewriteRule<FlattenAssocCommut>,
-      RewriteRule<AndSimplify>//,
-      //      RewriteRule<BitwiseSlicing>
+      RewriteRule<AndSimplify>,
+      RewriteRule<BitwiseSlicing>
       >::apply(node);
 
   if (resultNode.getKind() != node.getKind()) {
@@ -244,8 +244,8 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){
 
   resultNode = LinearRewriteStrategy
     < RewriteRule<FlattenAssocCommut>,
-      RewriteRule<OrSimplify>//,
-      //      RewriteRule<BitwiseSlicing>
+      RewriteRule<OrSimplify>,
+      RewriteRule<BitwiseSlicing>
     >::apply(node);
 
   if (resultNode.getKind() != node.getKind()) {
@@ -261,8 +261,8 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) {
   resultNode = LinearRewriteStrategy
     < RewriteRule<FlattenAssocCommut>, // flatten the expression 
       RewriteRule<XorSimplify>,        // simplify duplicates and constants
-      RewriteRule<XorZero>//,            // checks if the constant part is zero and eliminates it
-      //      RewriteRule<BitwiseSlicing>
+      RewriteRule<XorZero>,            // checks if the constant part is zero and eliminates it
+      RewriteRule<BitwiseSlicing>
     >::apply(node);
 
   // this simplification introduces new terms and might require further
-- 
2.30.2