From 63c361af66a911a519093f661ee42571417cf8ac Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 24 Feb 2011 02:00:15 +0000 Subject: [PATCH] Bugfix. The prior checkin added an assertion that didn't always hold. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1168 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/SubstitutionMap.cpp | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index f311282..a6e2565 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -103,16 +103,20 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a, ArrayTransform else// (IFF == k ) c1= simplify_during_create_subM ? simp->SimplifyFormula_NoRemoveWrites(c[1], false) : c[1]; - //fill the arrayname readindices vector if e0 is a - //READ(Arr,index) and index is a BVCONST - int to; - if ((to =TermOrder(c[0],c1))==1 && c[0].GetKind() == READ) - at->FillUp_ArrReadIndex_Vec(c[0], c1); - else if (to ==-1 && c1.GetKind() == READ) - at->FillUp_ArrReadIndex_Vec(c1,c[0]); - bool updated = UpdateSubstitutionMap(c[0], c1); output = updated ? ASTTrue : a; + + if (updated) + { + //fill the arrayname readindices vector if e0 is a + //READ(Arr,index) and index is a BVCONST + int to; + if ((to =TermOrder(c[0],c1))==1 && c[0].GetKind() == READ) + at->FillUp_ArrReadIndex_Vec(c[0], c1); + else if (to ==-1 && c1.GetKind() == READ) + at->FillUp_ArrReadIndex_Vec(c1,c[0]); + } + return output; } -- 2.47.3