From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 20 Oct 2009 21:28:12 +0000 (+0000)
Subject: minor edits
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=f46a6c4355927be41ffb8e32a5c17c25df00e759;p=francis%2Fstp.git

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 dfc05f0..42555a3 100644
--- 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 0d8e37b..6b210b7 100644
--- 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);