fixed the problem with Alvin Cheung's testcase. The problem was that ITE-array expres...

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 64fac5180d0a05bb620121fc335760cd1a23cd2b..85591d94bddaeb72abc7710e8d2ce9a99b7d1881 100644 (file)
--- 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 4d6ec08f7957eeabb84524c30ec51d511a1b1143..d05e1ac42cff89425c1b69f742e95ef72245477d 100644 (file)
--- 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()