From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 9 Jan 2012 13:49:57 +0000 (+0000)
Subject: Fix. Bad assertion,  thanks to Stephan Falke.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=0d26e7b299241a7e1f9b3c0d11072280fe597f90;p=francis%2Fstp.git

Fix. Bad assertion,  thanks to Stephan Falke.

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

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index edbaa6e..ca438ce 100644
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -1252,8 +1252,8 @@ namespace BEEV
         assert(products[i].size() == 1);
         results.push_back(products[i].back());
         }
-      assert(products[i+1].size() ==0); // i+1 is defined but should never be used.
 
+      assert(products[bitWidth].size() ==0); // i+1 is defined but should never be used.
       assert(results.size() == ((unsigned)bitWidth));
       return results;
     }