From fbc8c83444132e228cbf1b00cb5831d6e232288c Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 13 Aug 2011 21:48:23 +0000 Subject: [PATCH] Bugfix. Some array reads were not removed as is required. This caused an assertion error. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1387 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ArrayTransformer.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index 5f996de..3ca6d83 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -752,16 +752,16 @@ namespace BEEV */ if (ASTTrue == cond) { - result = TransformArrayRead(thnRead); + result = TransformTerm(thnRead); } else if (ASTFalse == cond) { - result = TransformArrayRead(elsRead); + result = TransformTerm(elsRead); } else { - thnRead = TransformArrayRead(thnRead); - elsRead = TransformArrayRead(elsRead); + thnRead = TransformTerm(thnRead); + elsRead = TransformTerm(elsRead); //(ITE cond (READ thn j) (READ els j)) result = simp->CreateSimplifiedTermITE(cond, thnRead, elsRead); -- 2.47.3