From 2d53a7cb745b6d6499f96f2e82c0d23294853e66 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 5 May 2010 16:31:35 +0000
Subject: [PATCH] fixed TEST_PREFIX in Makefile.common. Ideally this should be
 fixed in the configure script. Also added new testcase eric1.stp to the repo

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@745 e59a4935-1847-0410-ae03-e826735625c1
---
 scripts/Makefile.common       | 4 ++--
 src/STPManager/STP.cpp        | 4 +++-
 src/simplifier/simplifier.cpp | 2 ++
 3 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 8eea52f..a01953b 100644
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -16,7 +16,7 @@
 #OPTIMIZE      = -O3 -march=native -fomit-frame-pointer # Maximum optimization
 #OPTIMIZE      = -O3 -march=native -DNDEBUG -DLESSBYTES_PERNODE
 OPTIMIZE      = -O3               # Maximum optimization
-#CFLAGS_M32   = -m32
+CFLAGS_M32   = -m32
 CFLAGS_BASE   = $(OPTIMIZE)
 
 # OPTION to compile CRYPTOMiniSAT version 2.x
@@ -36,7 +36,7 @@ ifeq ($(SAT),minisat)
 endif
 
 # todo: These should be set by the config script of course..
-TEST_PREFIX=../stp-tests/
+TEST_PREFIX=../../stp-tests/
 SHELL=/bin/bash
 
 
diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 6e46846..95a8894 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -126,7 +126,9 @@ namespace BEEV {
     bm->ASTNodeStats("Before SimplifyWrites_Inplace begins: ", 
                      simplified_solved_InputToSAT);
 
-    bm->SimplifyWrites_InPlace_Flag = true;
+    //Vijay
+    //bm->SimplifyWrites_InPlace_Flag = true;
+    bm->SimplifyWrites_InPlace_Flag = false;
     bm->Begin_RemoveWrites = false;
     bm->start_abstracting = false;
     bm->TermsAlreadySeenMap_Clear();
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 9a693b1..4d6ec08 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2304,7 +2304,9 @@ namespace BEEV
               if (WRITE == inputterm[0].GetKind())
                 {
                   //get rid of all writes
+		  //_bm->ASTNodeStats("before RemoveWrites_TopLevel:", inputterm);
                   ASTNode nowrites = RemoveWrites_TopLevel(inputterm);
+		  //_bm->ASTNodeStats("after RemoveWrites_TopLevel:", nowrites);
                   out1 = nowrites;
                 }
               else if (ITE == inputterm[0].GetKind())
-- 
2.47.3