From 88b51082e8536c371890181cacecbc5c7e712e1d Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 31 Mar 2011 12:39:46 +0000
Subject: [PATCH] Small improvement. Discard the inner write if the two WRITEs
 are to the same index.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1247 e59a4935-1847-0410-ae03-e826735625c1
---
 src/AST/NodeFactory/SimplifyingNodeFactory.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index d47bb7a..ebd16ac 100644
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -870,6 +870,16 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
 		}
 		break;
 
+        case BEEV::WRITE:
+          if (children[0].GetKind() == BEEV::WRITE)
+          {
+              // If the indexes of two writes are the same, then discard the inner write.
+              if (children[1] == children[0][1])
+              {
+                  result = NodeFactory::CreateArrayTerm(BEEV::WRITE, children[0].GetIndexWidth(), children[0].GetValueWidth(),  children[0][0], children[1], children[2]);
+              }
+          }
+          break;
 
 	case BEEV::READ:
 	if (children[0].GetKind() == BEEV::WRITE)
-- 
2.47.3