minor edits

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@327 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index dfc05f0707bec0823c2f1df44a4310b9100746b2..42555a3d21df14c50793d6e70fc3bae659746622 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -926,7 +926,8 @@ namespace BEEV
   // complementing the result bit.
   ASTNode BitBlaster::BBBVLE(const ASTVec& left, 
                              const ASTVec& right,
-                            bool is_signed)
+                            bool is_signed,
+                            bool is_bvlt)
   {
     ASTVec::const_reverse_iterator lit    = left.rbegin();
     ASTVec::const_reverse_iterator litend = left.rend();
@@ -958,7 +959,10 @@ namespace BEEV
        prev_eq_bit = this_eq_bit;
       }
     
-    bit_comparisons.push_back(prev_eq_bit);
+    if(!is_bvlt)
+      {
+       bit_comparisons.push_back(prev_eq_bit);
+      }
     ASTNode output =
       _bm->CreateSimpForm(OR, bit_comparisons);
 
@@ -1090,7 +1094,7 @@ namespace BEEV
         }
       case BVLT:
         {
-          return _bm->CreateSimpNot(BBBVLE(right, left, false));
+          return BBBVLE(left, right, false, true);
           break;
         }
       case BVSLE:

diff --git a/src/to-sat/BitBlast.h b/src/to-sat/BitBlast.h
index 0d8e37b7a0ef398be55f65fe863a1e899c9ed375..6b210b7b0e38850d812bac58268dd763b8f87290 100644 (file)
--- a/src/to-sat/BitBlast.h
+++ b/src/to-sat/BitBlast.h
@@ -85,7 +85,8 @@ namespace BEEV
     ASTNode Sum(const ASTNode& xi, const ASTNode& yi, const ASTNode& cin);
 
     // Internal bit blasting routines.
-    ASTNode BBBVLE(const ASTVec& x, const ASTVec& y, bool is_signed);
+    ASTNode BBBVLE(const ASTVec& x, 
+                  const ASTVec& y, bool is_signed, bool is_bvlt = false);
 
     // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc.
     ASTNode BBcompare(const ASTNode& form);