From e6b57f37722186d71e493fdce5ca54b68d48e4cb Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 11 May 2011 03:34:42 +0000 Subject: [PATCH] Bugfix. Arithmetic shifts by constants that didn't fit in 32-bits would cause an assertion error. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1323 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/simplifier.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index f3f06a5..0a648df 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -1739,13 +1739,20 @@ namespace BEEV assert(b.isConstant()); assert(k == BVSRSHIFT); - const unsigned int shift = b.GetUnsignedConst(); - if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width) || (shift >= width)) + if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width)) { ASTNode top = bm.CreateBVConst(32,width-1); return nf->CreateTerm(BVSX, width, nf->CreateTerm(BVEXTRACT,1, children[0], top,top ), bm.CreateBVConst(32,width)); } + else + { + if (b.GetUnsignedConst() >= width) + { + ASTNode top = bm.CreateBVConst(32,width-1); + return nf->CreateTerm(BVSX, width, nf->CreateTerm(BVEXTRACT,1, children[0], top,top ), bm.CreateBVConst(32,width)); + } + } return ASTNode(); } -- 2.47.3