From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 8 Jun 2010 12:52:46 +0000 (+0000)
Subject: Bugfix. The bvsolver would replace a variable with an equation that contained that... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=773544551995dfe40aaf9fd76176109c24489a98;p=francis%2Fstp.git

Bugfix. The bvsolver would replace a variable with an equation that contained that same variable. It did so because there was a special case that let it. I removed the special case.

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 3d74532..dad5d27 100644
--- 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;