From 085e39e00eba5c2c553de0c5764573781913d182 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 23 Feb 2011 14:11:31 +0000 Subject: [PATCH] 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 --- src/AST/ArrayTransformer.cpp | 2 +- src/absrefine_counterexample/AbstractionRefinement.cpp | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index 78cded9..23ed705 100644 --- 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 40ece0c..6a1aeaa 100644 --- a/src/absrefine_counterexample/AbstractionRefinement.cpp +++ b/src/absrefine_counterexample/AbstractionRefinement.cpp @@ -81,21 +81,21 @@ namespace BEEV vector concreteValues; concreteValues.reserve(mapper.size()); - int i =0; for (map::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()); -- 2.47.3