Commit b3e6cb30 by Alan Mishchenko

Bug fix in %read_smt and prevent crash of &cec if there is no current AIG.

parent c0f0e145
...@@ -31034,6 +31034,11 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -31034,6 +31034,11 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage; goto usage;
} }
} }
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no AIG.\n" );
return 1;
}
if ( fMiter ) if ( fMiter )
{ {
if ( fDualOutput ) if ( fDualOutput )
...@@ -290,10 +290,20 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits ...@@ -290,10 +290,20 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits
Vec_Int_t * vFanins = Vec_IntAlloc( 10 ); Vec_Int_t * vFanins = Vec_IntAlloc( 10 );
if ( pStr[0] != '#' ) // decimal if ( pStr[0] != '#' ) // decimal
{ {
int Number = atoi( pStr ); if ( pStr[0] >= 0 && pStr[0] <= 9 )
nBits = Abc_Base2Log( Number+1 ); {
assert( nBits < 32 ); int Number = atoi( pStr );
Vec_IntPush( vFanins, Number ); nBits = Abc_Base2Log( Number+1 );
assert( nBits < 32 );
Vec_IntPush( vFanins, Number );
}
else
{
int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
assert( fFound );
Vec_IntFree( vFanins );
return iObj;
}
} }
else if ( pStr[1] == 'b' ) // binary else if ( pStr[1] == 'b' ) // binary
{ {
......
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