From aec81b61712d48d96c0f702d53c317d4612c8619 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 9 Mar 2010 14:51:16 +0000 Subject: [PATCH] Allow lefshift by zero. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@633 e59a4935-1847-0410-ae03-e826735625c1 --- src/parser/CVC.y | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/parser/CVC.y b/src/parser/CVC.y index 97dedea..eeb4a1d 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -911,6 +911,12 @@ Expr : TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->Reso } | Expr BVLEFTSHIFT_TOK NUMERAL_TOK { + if (0 == $3) + { + $$ = $1; + } + else + { ASTNode zero_bits = ParserBM->CreateZeroConst($3); ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVCONCAT, @@ -918,6 +924,7 @@ Expr : TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->Reso BVTypeCheck(*n); $$ = n; delete $1; + } } /* | Expr BVLEFTSHIFT_TOK Expr */ /* { */ -- 2.47.3