git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk...

diff --git a/src/AST/AST.h b/src/AST/AST.h
index cd1be0ca1ba248e84ce2e58fd18dddf3f56971e6..fff6f7662dcecceeefdb2121984128f3bafc851d 100644 (file)
--- 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 c8f3358f53617db2e35a176a8eefec065c8060bb..a46d95a6700ad887378781245a94e5e6091b6e51 100644 (file)
--- 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";