Bugfix. The bvsolver would replace a variable with an equation that contained that...

I don't understand why the special case was there, so aren't sure if this will slow down some other instances?

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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 3d74532e7b821ea3c3c16500239b27bbfbabd82e..dad5d27c1a760d3579d3ef2b61e7c1159688c965 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -926,14 +926,30 @@ namespace BEEV
         && WRITE == term[0].GetKind() 
         && !_bm->GetRemoveWritesFlag())
       {
-        return false;
+       /*
+               Trevor: This used to return false. But fails on the below input.
+               I don't know why the case of read-over-write was handled specially.
+
+
+               Printing: after simplification:
+               30:(EQ
+                 12:b3
+                 26:(READ
+                       22:(WRITE
+                         14:a3
+                         18:0b0000000000
+                         18:0b0000000000)
+                       12:b3))
+        */
+
+       //return false;
       }
 
     if (READ == term.GetKind() 
         && WRITE == term[0].GetKind() 
         && _bm->GetRemoveWritesFlag())
       {
-        return true;
+        //return true;
       }
 
     ASTNodeMap::iterator it;