Improvement. Exit-after-cnf would exit after sending the CNF to the SAT solver. We...

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

diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp
index 011e5b2eb1389a74a08bd51654c58130d07f7e42..63b9659347a534a9a2b6c6a9c4bd9fcdc45a14d4 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.cpp
+++ b/src/to-sat/AIG/ToSATAIG.cpp
@@ -72,6 +72,18 @@ namespace BEEV
       }
          first = false;
 
+      if (bm->UserFlags.exit_after_CNF)
+            {
+              if (bm->UserFlags.quick_statistics_flag)
+                bm->GetRunTimes()->print();
+
+              if (needAbsRef)
+                cerr << "Warning: STP is exiting after generating the first CNF. But the CNF"
+                " is probably partial which you probably don't want. You probably want to disable"
+                " refinement with the \"-r\" command line option." << endl;
+
+              exit(0);
+            }
 
       bm->GetRunTimes()->start(RunTimes::SendingToSAT);
 
@@ -119,18 +131,6 @@ namespace BEEV
          toCNF.setPrior(cnfData);
       }
 
-      if (bm->UserFlags.exit_after_CNF)
-      {
-        if (bm->UserFlags.quick_statistics_flag)
-          bm->GetRunTimes()->print();
-
-        if (needAbsRef)
-          cerr << "Warning: STP is exiting after generating the first CNF. But the CNF"
-          "is probably partial which you probably don't want. You probably want to disable"
-          "refinement with the \"-r\" command line option." << endl;
-
-        exit(0);
-      }
 
       bm->GetRunTimes()->start(RunTimes::Solving);
       satSolver.solve();