updated the author name

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 035bd4469bb0c68e2ace1de449db081711a88407..2da4dfa6ab1f3b389a709ff72a38ec00e7a406e3 100644 (file)
--- 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 44c498947315a8554fa4c48acd493309e3282447..0775cb1f8292ef441621e327c905ae2a0cb1be6f 100644 (file)
--- 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