From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 6 May 2010 17:06:42 +0000 (+0000)
Subject: fixed the problem with Alvin Cheung's testcase. The problem was that ITE-array expres... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=b8405619a957d5c315d587892ff7ce8a056d31f3;p=francis%2Fstp.git

fixed the problem with Alvin Cheung's testcase. The problem was that ITE-array expressions were not being handled correctly in SimplifyWrite_InPlace(). Fixed that

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

diff --git a/README b/README
index 64fac51..85591d9 100644
--- a/README
+++ b/README
@@ -51,7 +51,7 @@ REGRESSIONS
 
 Assumes you have downloaded the testcases as follows:
 
-svn co https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/stp-tests/test
+svn co https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/stp-tests
 
 
 make regresssmt
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 4d6ec08..d05e1ac 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2927,6 +2927,7 @@ namespace BEEV
 
     ASTVec writeIndices, writeValues;
     unsigned int width = term.GetValueWidth();
+    ASTNode original_write = term[0];
     ASTNode write = term[0];
     unsigned indexwidth = write.GetIndexWidth();
     ASTNode readIndex = SimplifyTerm(term[1]);
@@ -2984,7 +2985,6 @@ namespace BEEV
     ASTVec::reverse_iterator itend_values = writeValues.rend();
 
     // May be a symbol, or an ITE.
-
     for (; it_index != itend_index; it_index++, it_values++)
       {
         write = _bm->CreateTerm(WRITE, width, write, *it_index, *it_values);
@@ -2992,6 +2992,13 @@ namespace BEEV
       }
 
     output = _bm->CreateTerm(READ, width, write, readIndex);
+    assert(BVTypeCheck(output));
+    if(ITE == write.GetKind())
+      {
+	output = SimplifyTerm(output, VarConstMap);
+      }
+
+    //UpdateSimplifyMap(original_write, write, false);
     UpdateSimplifyMap(term, output, false);
     return output;
   } //end of SimplifyWrites_In_Place()