From 9aec7f619dbc1681758e206f3bbfb56f65cd65bc Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 9 Nov 2009 16:52:56 +0000
Subject: [PATCH] calling CRYPTOMINISAT Simplify() before calling Solve()

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@395 e59a4935-1847-0410-ae03-e826735625c1
---
 src/to-sat/ToSAT.cpp | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 1f774d5..8f62a51 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -131,7 +131,10 @@ bool isTseitinVariable(const ASTNode& n) {
             //           << percentage << endl;
             bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
             bm->GetRunTimes()->start(RunTimes::Solving);
-            newS.solve();
+#ifdef CRYPTOMINISAT
+	    if (newS.simplify() == MINISAT::l_Undef)
+#endif
+	      newS.solve();
             bm->GetRunTimes()->stop(RunTimes::Solving);
             if(!newS.okay())
               {
@@ -155,7 +158,10 @@ bool isTseitinVariable(const ASTNode& n) {
 
     bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
     bm->GetRunTimes()->start(RunTimes::Solving);
-    newS.solve();
+#ifdef CRYPTOMINISAT
+    if (newS.simplify() == MINISAT::l_Undef)
+#endif
+      newS.solve();
     bm->GetRunTimes()->stop(RunTimes::Solving);
     bm->PrintStats(newS);
     if (newS.okay())
-- 
2.47.3