diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 8c378569f..abd668c62 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -36,111 +36,6 @@ static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncreme
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/**Function*************************************************************
-
-  Synopsis    [Write the clauses in the solver into a file in DIMACS format.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
-{
-    Sat_Mem_t * pMem = &p->Mem;
-    FILE * pFile;
-    clause * c;
-    int i, k;
-
-    // start the file
-    pFile = fopen( pFileName, "wb" );
-    if ( pFile == NULL )
-    {
-        printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
-        return;
-    }
-//    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
-    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0) );
-
-    // write the original clauses
-    Sat_MemForEachClause( pMem, c, i, k )
-        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
-
-    // write the learned clauses
-    Sat_MemForEachLearned( pMem, c, i, k )
-        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
-
-    // write zero-level assertions
-    for ( i = 0; i < p->size; i++ )
-        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
-            fprintf( pFile, "%s%d%s\n",
-                     (p->assigns[i] == l_False)? "-": "",
-                     i + (int)(incrementVars>0),
-                     (incrementVars) ? " 0" : "");
-
-    // write the assumptions
-    if (assumptionsBegin) {
-        for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
-            fprintf( pFile, "%s%d%s\n",
-                     lit_sign(*assumptionsBegin)? "-": "",
-                     lit_var(*assumptionsBegin) + (int)(incrementVars>0),
-                     (incrementVars) ? " 0" : "");
-        }
-    }
-
-    fprintf( pFile, "\n" );
-    fclose( pFile );
-} 
-void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
-{
-    Sat_Mem_t * pMem = &p->Mem;
-    FILE * pFile;
-    clause * c;
-    int i, k;
-
-    // start the file
-    pFile = fopen( pFileName, "wb" );
-    if ( pFile == NULL )
-    {
-        printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
-        return;
-    }
-//    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
-    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0) );
-
-    // write the original clauses
-    Sat_MemForEachClause2( pMem, c, i, k )
-        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
-
-    // write the learned clauses
-    Sat_MemForEachLearned( pMem, c, i, k )
-        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
-
-    // write zero-level assertions
-    for ( i = 0; i < p->size; i++ )
-        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
-            fprintf( pFile, "%s%d%s\n",
-                     (p->assigns[i] == l_False)? "-": "",
-                     i + (int)(incrementVars>0),
-                     (incrementVars) ? " 0" : "");
-
-    // write the assumptions
-    if (assumptionsBegin) {
-        for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
-            fprintf( pFile, "%s%d%s\n",
-                     lit_sign(*assumptionsBegin)? "-": "",
-                     lit_var(*assumptionsBegin) + (int)(incrementVars>0),
-                     (incrementVars) ? " 0" : "");
-        }
-    }
-
-    fprintf( pFile, "\n" );
-    fclose( pFile );
-}   
-  
-
 /**Function*************************************************************
 
   Synopsis    [Writes the given clause in a file in DIMACS format.]
@@ -162,6 +57,123 @@ void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
     fprintf( pFile, "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Write the clauses in the solver into a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin, lit* assumpEnd, int incrementVars )
+{
+    Sat_Mem_t * pMem = &p->Mem;
+    FILE * pFile;
+    clause * c;
+    int i, k, nUnits;
+
+    // count the number of unit clauses
+    nUnits = 0;
+    for ( i = 0; i < p->size; i++ )
+        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+            nUnits++;
+
+    // start the file
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
+        return;
+    }
+//    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
+    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(assumpEnd-assumpBegin) );
+
+    // write the original clauses
+    Sat_MemForEachClause( pMem, c, i, k )
+        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
+
+    // write the learned clauses
+    Sat_MemForEachLearned( pMem, c, i, k )
+        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
+
+    // write zero-level assertions
+    for ( i = 0; i < p->size; i++ )
+        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+            fprintf( pFile, "%s%d%s\n",
+                     (p->assigns[i] == l_False)? "-": "",
+                     i + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+
+    // write the assump
+    if (assumpBegin) {
+        for (; assumpBegin != assumpEnd; assumpBegin++) {
+            fprintf( pFile, "%s%d%s\n",
+                     lit_sign(*assumpBegin)? "-": "",
+                     lit_var(*assumpBegin) + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+        }
+    }
+
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+} 
+void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin, lit* assumpEnd, int incrementVars )
+{
+    Sat_Mem_t * pMem = &p->Mem;
+    FILE * pFile;
+    clause * c;
+    int i, k, nUnits;
+
+    // count the number of unit clauses
+    nUnits = 0;
+    for ( i = 0; i < p->size; i++ )
+        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+            nUnits++;
+
+    // start the file
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
+        return;
+    }
+//    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
+    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(assumpEnd-assumpBegin) );
+
+    // write the original clauses
+    Sat_MemForEachClause2( pMem, c, i, k )
+        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
+
+    // write the learned clauses
+    Sat_MemForEachLearned( pMem, c, i, k )
+        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
+
+    // write zero-level assertions
+    for ( i = 0; i < p->size; i++ )
+        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+            fprintf( pFile, "%s%d%s\n",
+                     (p->assigns[i] == l_False)? "-": "",
+                     i + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+
+    // write the assump
+    if (assumpBegin) {
+        for (; assumpBegin != assumpEnd; assumpBegin++) {
+            fprintf( pFile, "%s%d%s\n",
+                     lit_sign(*assumpBegin)? "-": "",
+                     lit_var(*assumpBegin) + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+        }
+    }
+
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}   
+  
+
 /**Function*************************************************************
 
   Synopsis    [Writes the given clause in a file in DIMACS format.]