From: lianah <lianahady@gmail.com>
Date: Tue, 30 Apr 2013 20:39:52 +0000 (-0400)
Subject: merged cvc4 master
X-Git-Tag: cvc5-1.0.0~7294
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2d9b058a6a5c977f2806965526320e6d5fed18fe;p=cvc5.git

merged cvc4 master
---

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index b2f91e070..9c64cbf77 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -180,7 +180,7 @@ void TheoryBV::check(Effort e)
   
   while (!done()) {
     TNode fact = get().assertion;
-    checkForLemma(fact); 
+    // checkForLemma(fact); 
     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
       d_subtheories[i]->assertFact(fact); 
     }
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 0775cb1f8..5a43e2c57 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -106,16 +106,16 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){
       RewriteRule<UleMax>,
       RewriteRule<ZeroUle>,
       RewriteRule<UleZero>,
-      RewriteRule<UleSelf>,
-      RewriteRule<UleEliminate>
+      RewriteRule<UleSelf>//,
+      //      RewriteRule<UleEliminate>
       >::apply(node);
   return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode); 
 }
 
 RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){
   Node resultNode = LinearRewriteStrategy
-    < RewriteRule <EvalSle>, 
-      RewriteRule <SleEliminate>
+    < RewriteRule <EvalSle>//, 
+      //      RewriteRule <SleEliminate>
       >::apply(node);
   return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode); 
 }