From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 24 Feb 2011 02:00:15 +0000 (+0000)
Subject: Bugfix. The prior checkin added an assertion that didn't always hold.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=63c361af66a911a519093f661ee42571417cf8ac;p=francis%2Fstp.git

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
---

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;
     }