Commit 3d8eff2c by Alan Mishchenko

Corner-cases in &gprove and &mprove.

parent ebf10fdc
...@@ -32709,6 +32709,11 @@ int Abc_CommandAbc9GroupProve( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -32709,6 +32709,11 @@ int Abc_CommandAbc9GroupProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9GroupProve(): There is no AIG.\n" ); Abc_Print( -1, "Abc_CommandAbc9GroupProve(): There is no AIG.\n" );
return 1; return 1;
} }
if ( pCommLine == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9GroupProve(): Command line is not given.\n" );
return 1;
}
vStatus = Gia_ManGroupProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose ); vStatus = Gia_ManGroupProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose );
Vec_IntFree( vStatus ); Vec_IntFree( vStatus );
return 0; return 0;
...@@ -32826,7 +32831,12 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -32826,7 +32831,12 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
if ( pAbc->pGia == NULL ) if ( pAbc->pGia == NULL )
{ {
Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" ); Abc_Print( -1, "Abc_CommandAbc9MultiProve(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "Abc_CommandAbc9MultiProve(): The problem is combinational.\n" );
return 1; return 1;
} }
pAbc->Status = Gia_ManMultiProve( pAbc->pGia, pPars ); pAbc->Status = Gia_ManMultiProve( pAbc->pGia, pPars );
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment