switched bv equality order

diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index 649af5ff987557c1dd6e21452889efb6351f6b7d..43acfef7567cff42ec5e685e710884b7034fbf0e 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -270,7 +270,7 @@ Node RewriteRule<SimplifyEq>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<ReflexivityEq>::applies(TNode node) {
-  return (node.getKind() == kind::EQUAL && node[0] > node[1]);
+  return (node.getKind() == kind::EQUAL && node[0] < node[1]);
 }
 
 template<> inline

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index b13172bfaa3b1e86ed8544f56ff7a2a5425d606a..0807b3d66023d767d54aaefe39d91f1ea0c587ea 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -684,7 +684,7 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
     return utils::mkTrue();
   }
 
-  if (newLeft > newRight) {
+  if (newLeft < newRight) {
     Assert((newRight == left && newLeft == right) ||
            Rewriter::rewrite(newRight) != left ||
            Rewriter::rewrite(newLeft) != right);

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 6fd3bbf9276844398d6e9726db3400accaf1f8f6..4a0da44ccda01b1e1d33943e02ac61eddb2075fe 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -60,20 +60,7 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
   if(res.node!= node) {
     Debug("bitvector-rewrite") << "TheoryBV::postRewrite    " << node << std::endl;
     Debug("bitvector-rewrite") << "TheoryBV::postRewrite to " << res.node << std::endl;
-    if (res.node.getKind() == kind::EQUAL) {
-      Assert (res.node[0] < res.node[1]); 
-    }
-  }
-  if (res.node.getKind() == kind::EQUAL) {
-    Assert (res.node[0] < res.node[1]); 
   }
-
-  // if (res.status == REWRITE_DONE) {
-  //   Node rewr = res.node;
-  //   Node rerewr = d_rewriteTable[rewr.getKind()](rewr, false).node;
-  //   Assert(rewr == rerewr);
-  // }
-  
   return res; 
 }