From b8a60f34b4ad8ceca5213c7a48a0d687e196dfcb Mon Sep 17 00:00:00 2001 From: katelman Date: Mon, 17 May 2010 18:31:51 +0000 Subject: [PATCH] BOOLEXTRACT seems to have been implemented backward. It did an equality test on the extracted bit against *zero*, instead of *one*. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@768 e59a4935-1847-0410-ae03-e826735625c1 --- src/parser/CVC.y | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/parser/CVC.y b/src/parser/CVC.y index 65fe8a1..c5dedc0 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -468,8 +468,8 @@ Formula : '(' Formula ')' ASTNode hi = parserInterface->CreateBVConst(32, $5); ASTNode low = parserInterface->CreateBVConst(32, $5); ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVEXTRACT,1,*$3,hi,low)); - ASTNode zero = parserInterface->CreateBVConst(1,0); - ASTNode * out = new ASTNode(parserInterface->nf->CreateNode(EQ,*n,zero)); + ASTNode one = parserInterface->CreateBVConst(1,1); + ASTNode * out = new ASTNode(parserInterface->nf->CreateNode(EQ,*n,one)); $$ = out; -- 2.47.3