From 7a1c24e768bf9f08b49f778ba7cf77ce9271d121 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 24 May 2010 02:09:23 +0000 Subject: [PATCH] Bugfix. Rare types of array reads were causing a type-error. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@784 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ArrayTransformer.cpp | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index f47454b..dc63a2b 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -730,24 +730,29 @@ namespace BEEV const ASTNode& thn = arrName[1]; const ASTNode& els = arrName[2]; + //(READ thn j) + ASTNode thnRead = nf->CreateTerm(READ, width, thn, readIndex); + assert(BVTypeCheck(thnRead)); + + //(READ els j) + ASTNode elsRead = nf->CreateTerm(READ, width, els, readIndex); + assert(BVTypeCheck(elsRead)); + + /* We try to call TransformArrayRead only if necessary, because it + * introduces a new symbol for each read. The amount of work we + * need to do later is based on the square of the number of symbols. + */ if (ASTTrue == cond) { - result = TransformTerm(thn); + result = TransformArrayRead(thnRead); } else if (ASTFalse == cond) { - result = TransformTerm(els); + result = TransformArrayRead(elsRead); } else { - //(READ thn j) - ASTNode thnRead = nf->CreateTerm(READ, width, thn, readIndex); - assert(BVTypeCheck(thnRead)); thnRead = TransformArrayRead(thnRead); - - //(READ els j) - ASTNode elsRead = nf->CreateTerm(READ, width, els, readIndex); - assert(BVTypeCheck(elsRead)); elsRead = TransformArrayRead(elsRead); //(ITE cond (READ thn j) (READ els j)) -- 2.47.3