From 093ddd405926a5fda10da311699b34cf89c45b51 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 27 Sep 2009 19:26:38 +0000
Subject: [PATCH] git-svn-id:
 https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@261
 e59a4935-1847-0410-ae03-e826735625c1

---
 src/AST/AST.h                        |  1 +
 src/AST/printer/AssortedPrinters.cpp | 19 ++++++++++++++++---
 2 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/src/AST/AST.h b/src/AST/AST.h
index cd1be0c..fff6f76 100644
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -1606,6 +1606,7 @@ namespace BEEV
   public:
     ASTVec ListOfDeclaredVars;
     void printVarDeclsToStream(ostream &os);
+    void printAssertsToStream(ostream &os, int simplify);
 
     // Constructor
     BeevMgr() :
diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp
index c8f3358..a46d95a 100644
--- a/src/AST/printer/AssortedPrinters.cpp
+++ b/src/AST/printer/AssortedPrinters.cpp
@@ -391,11 +391,24 @@ namespace BEEV
     }
   } //printVarDeclsToStream
 
+
+
+  void BeevMgr::printAssertsToStream(ostream &os, int simplify_print) {
+  ASTVec v = GetAsserts();
+  for(ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) {
+    Begin_RemoveWrites = true;
+    ASTNode q = (simplify_print == 1) ? SimplifyFormula_TopLevel(*i,false) : *i;
+    q = (simplify_print == 1) ? SimplifyFormula_TopLevel(q,false) : q;
+    Begin_RemoveWrites = false;
+    os << "ASSERT( ";
+    q.PL_Print(os);
+    os << ");" << endl;
+  }
+}
+
   void print_STPInput_Back(const ASTNode& asserts, const ASTNode& query) {
     BEEV::GlobalBeevMgr->printVarDeclsToStream(cout);
-    cout << "ASSERT(";
-    asserts.PL_Print(cout);
-    cout << ");\n\n";
+    BEEV::GlobalBeevMgr->printAssertsToStream(cout,0);
     cout << "QUERY(";
     query.PL_Print(cout);
     cout << ");\n";
-- 
2.47.3