Bugfix. Fix the prior checkin.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1162 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 78cded97b8cf903c52b4e6de366ab551c1312b5c..23ed705fa7aad15910d63cc1ae505dfb75754c88 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -825,7 +825,7 @@ namespace BEEV
         (*Arrayname_ReadindicesMap)[e0[0]].push_back(e0[1]);
         //e0 is the array read : READ(A,i) and e1 is a bvconst
         Arrayread_SymbolMap[e0] = e1;
-        arrayToIndexToRead[e0[0]].insert(make_pair(e0[1],ArrayRead (e0[1], e0[1])));
+        arrayToIndexToRead[e0[0]].insert(make_pair(e0[1],ArrayRead (e1, e1)));
         return;
       }
 

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index 40ece0ca2c6a51fee97c9443461d1e8c85e0f1b7..6a1aeaa161e3d0a76fa0356a77fbb052eabf45db 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -81,21 +81,21 @@ namespace BEEV
        vector<ASTNode> concreteValues;
        concreteValues.reserve(mapper.size());
 
-       int i =0;
        for (map<ASTNode, ArrayTransformer::ArrayRead>::const_iterator it =mapper.begin() ; it != mapper.end();it++)
        {
-
            const ASTNode& the_index = it->first;
-            listOfIndices.push_back(it->first);
+            listOfIndices.push_back(the_index);
 
             ASTNode arrsym = it->second.symbol;
             read_node_symbols.push_back(arrsym);
 
+                       assert(read_node_symbols[0].GetValueWidth() == arrsym.GetValueWidth());
+                       assert(listOfIndices[0].GetValueWidth() == the_index.GetValueWidth());
+
             jKind.push_back(the_index.GetKind());
 
             concreteIndexes.push_back(TermToConstTermUsingModel(the_index));
             concreteValues.push_back(TermToConstTermUsingModel(arrsym));
-            i++;
        }
 
        assert(listOfIndices.size() == mapper.size());