From 00cfb06c78c2614907f3d42950f99419e47ccfc1 Mon Sep 17 00:00:00 2001 From: katelman Date: Tue, 30 Dec 2008 06:17:29 +0000 Subject: [PATCH] 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 --- AST/ToSAT.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/AST/ToSAT.cpp b/AST/ToSAT.cpp index 9e8623e..3a73fc8 100644 --- 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 { -- 2.47.3