Fixed correctness bug in TermToConstTermUsingModel. CounterExampleMap

originally gets a copy of SubstitutionMap by way of SolverMap, and since
SubstitutionMap may not have fully reduced terms, we need to call
TermToConstTermUsingModel on anything read from CounterExampleMap. This was not
done for an array read case.

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

diff --git a/AST/ToSAT.cpp b/AST/ToSAT.cpp
index 9e8623ef724e5a49e05658e4ae76ef6fba745332..3a73fc88301b4881be5be6ab9e6fb7aa4e896324 100644 (file)
--- a/AST/ToSAT.cpp
+++ b/AST/ToSAT.cpp
@@ -503,7 +503,8 @@ namespace BEEV {
       ASTNode modelentry;
       if(CounterExampleMap.find(index) != CounterExampleMap.end()) {   
        //index has a const value in the CounterExampleMap
-       ASTNode indexVal = CounterExampleMap[index];
+       //ASTNode indexVal = CounterExampleMap[index];
+   ASTNode indexVal = TermToConstTermUsingModel(CounterExampleMap[index], ArrayReadFlag);
        modelentry = CreateTerm(READ, arrName.GetValueWidth(), arrName, indexVal);
       }
       else {