3 files changed, 7 insertions, 7 deletions
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 1d94d685..a8cd3f7e 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -85,7 +85,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin,
             nUnits++;
 
     // start the file
-    pFile = fopen( pFileName, "wb" );
+    pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
     if ( pFile == NULL )
     {
         printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
@@ -121,7 +121,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin,
     }
 
     fprintf( pFile, "\n" );
-    fclose( pFile );
+    if ( pFileName ) fclose( pFile );
 } 
 void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin, lit* assumpEnd, int incrementVars )
 {
diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h
index 6c6cbeb3..01728c81 100644
--- a/src/sat/cnf/cnf.h
+++ b/src/sat/cnf/cnf.h
@@ -156,7 +156,7 @@ extern Cnf_Dat_t *     Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses,
 extern Cnf_Dat_t *     Cnf_DataDup( Cnf_Dat_t * p );
 extern void            Cnf_DataFree( Cnf_Dat_t * p );
 extern void            Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
-extern Vec_Int_t *     Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar );
+extern void            Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec_Int_t * vFlips );
 extern void            Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits );
 extern void            Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vForAlls, Vec_Int_t * vExists );
diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c
index d3a8aa9c..5a125ec3 100644
--- a/src/sat/cnf/cnfMan.c
+++ b/src/sat/cnf/cnfMan.c
@@ -215,14 +215,14 @@ void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus )
     for ( v = 0; v < p->nLiterals; v++ )
         p->pClauses[0][v] += 2*nVarsPlus;
 }
-Vec_Int_t * Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar )
+void Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec_Int_t * vFlips )
 {
-    Vec_Int_t * vLits = Vec_IntAlloc( 100 ); int v;
+    int v;
     assert( p->pMan == NULL );
+    Vec_IntClear( vFlips );
     for ( v = 0; v < p->nLiterals; v++ )
         if ( Abc_Lit2Var(p->pClauses[0][v]) == iFlipVar )
-            Vec_IntPush( vLits, v );
-    return vLits;
+            Vec_IntPush( vFlips, v );
 }
 void Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits )
 {