fixed TEST_PREFIX in Makefile.common. Ideally this should be fixed in the configure...

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 8eea52fc423db8758ed3e9b41bcd5a3ce0e6755e..a01953bfb3770619160d955e4edbf51d03949c34 100644 (file)
--- 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 6e46846e869226742f746cbe2ed59b7be6c413c8..95a8894d7e3576641617977d812817e12fc79fe6 100644 (file)
--- 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 9a693b12b76d6673d14f201ee3e49ae58ad5d93c..4d6ec08f7957eeabb84524c30ec51d511a1b1143 100644 (file)
--- 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())