Tuning SAT solver for QBF instances.

src/base/abci/abc.c

@@ -21839,7 +21839,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
         fclose( pFile );
-        Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, &pModel, Abc_NtkPiNum(pNtk) );
+        Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, &pModel, pNtk ? Abc_NtkPiNum(pNtk) : 0 );
         if ( pModel && pNtk )
         {
             int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pModel );

src/sat/cnf/cnfUtil.c

@@ -449,7 +449,7 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart,
     //Abc_Print( -1, "\n" );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     // derive SAT assignment
-    if ( RetValue == 0 )
+    if ( RetValue == 0 && nPis > 0 )
     {
         *ppModel = ABC_ALLOC( int, nPis );
         for ( i = 0; i < nPis; i++ )