From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 11 May 2011 04:23:04 +0000 (+0000)
Subject: Improvement. Exit-after-cnf would exit after sending the CNF to the SAT solver. We... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=823166d849e5117762d8b6a7457339ae78c4a452;p=francis%2Fstp.git

Improvement. Exit-after-cnf would exit after sending the CNF to the SAT solver. We used to read the CNF back out of the SAT solver, but don't any longer, so there's no reason to do this.



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 011e5b2..63b9659 100644
--- 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();