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

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 1f774d59e2cbb529d3fc08b71164e141ee35dc86..8f62a516bbbe0ab480c7bc646cc8187d627c58e7 100644 (file)
--- 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())