From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 15 Sep 2009 13:57:42 +0000 (+0000)
Subject: Fixes an off-by-one defect introduced in #230
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=6ce32edae73d1bace9af1d19f70f087a49699f5f;p=francis%2Fstp.git

Fixes an off-by-one defect introduced in #230



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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 7513942..9db6418 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2159,8 +2159,8 @@ ASTNode Flatten(const ASTNode& a)
 						else if (k == BVRIGHTSHIFT)
 						{
 							ASTNode zero = CreateZeroConst(shift);
-							ASTNode hi = CreateBVConst(32, width );
-							ASTNode low = CreateBVConst(32, shift+1);
+							ASTNode hi = CreateBVConst(32, width -1);
+							ASTNode low = CreateBVConst(32, shift);
 							ASTNode extract = CreateTerm(BVEXTRACT, width - shift, a, hi, low);
 							BVTypeCheck(extract);
 							output = CreateTerm(BVCONCAT, width, zero, extract);