From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 8 Dec 2009 17:24:48 +0000 (+0000)
Subject: added cnf dumping facility
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=919851e083c8769164f9538631d3059c6ed9b22c;p=francis%2Fstp.git

added cnf dumping facility

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index d04d5ca..3e710a3 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -21,11 +21,16 @@ namespace BEEV {
 					    bm->CreateNode(NOT, query));
     
     //solver instantiated here
-#ifdef CORE
+#if defined CORE || defined CRYPTOMINISAT
     MINISAT::Solver NewSolver;
 #endif
-#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
+#if defined CRYPTOMINISAT2
     MINISAT::Solver NewSolver;
+    if(bm->UserFlags.print_cnf_flag)
+      {
+	newS.needLibraryCNFFile("output.cnf");
+      }
+
 #endif
 #ifdef SIMP
     MINISAT::SimpSolver NewSolver;
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 6f44a3c..579fa50 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -90,10 +90,6 @@ namespace BEEV
 #endif
       }
 
-    if(bm->UserFlags.print_cnf_flag)
-      {
-	//newSolver.cnfDump = true;
-      }
 #ifdef CRYPTOMINISAT
     newSolver.startClauseAdding();
 #endif