1 files changed, 10 insertions, 1 deletions
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index ad595ab9..9c23e0d0 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -818,7 +818,7 @@ void Glucose_ReadDimacs( char * pFileName, SimpSolver& s )
   SeeAlso     []
 
 ***********************************************************************/
-void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars )
+void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars, int fDumpCnf )
 {
     abctime clk = Abc_Clock();
 
@@ -844,6 +844,15 @@ void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars )
         S.eliminate(true);
         printf( "c Simplication removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+        if ( fDumpCnf )
+        {
+            char * pFileCnf = Extra_FileNameGenericAppend( pFileName, "_out.cnf" );
+            S.toDimacs(pFileCnf);
+            printf( "Finished dumping CNF after preprocessing into file \"%s\".\n", pFileCnf );
+            printf( "SAT solving is not performed.\n" );
+            return;
+        }
     }
 
     vec<Lit> dummy;