diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-21 20:47:47 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-21 20:47:47 -0700 |
| commit | 17718a4c7d32714c354bb6dd56fcda83d4c44600 (patch) | |
| tree | 64686b366e474a52703a7ea89831136a6e9e29d5 /src/sat | |
| parent | ce232aca4e507d24261256aaaefe55f306494d0d (diff) | |
| download | abc-17718a4c7d32714c354bb6dd56fcda83d4c44600.tar.gz abc-17718a4c7d32714c354bb6dd56fcda83d4c44600.tar.bz2 abc-17718a4c7d32714c354bb6dd56fcda83d4c44600.zip | |
Corner case bug in 'satclp'.
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bmc/bmcClp.c | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index 140accf8..fff4d75f 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -499,7 +499,7 @@ Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCan Vec_Int_t * vLits = Vec_IntAlloc( nVars ); Vec_Int_t * vNums = Vec_IntAlloc( nVars ); Vec_Int_t * vCube = Vec_IntAlloc( nVars ); - int n, v, iVar, iLit, iCiVarBeg, iCube, Start, status; + int n, v, iVar, iLit, iCiVarBeg, iCube = 0, Start, status; abctime clk = 0, Time[2][2] = {{0}}; int fComplete[2] = {0}; @@ -521,7 +521,9 @@ Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCan goto cleanup; // timeout if ( status == l_False ) { - Vec_StrPrintStr( vSop[0], n ? " 1\n\0" : " 0\n\0" ); + Vec_StrClear( vSop[0] ); + Vec_StrPrintStr( vSop[0], n ? " 1\n" : " 0\n" ); + Vec_StrPush( vSop[0], '\0' ); fComplete[0] = 1; goto cleanup; // const0/1 } @@ -620,7 +622,8 @@ cleanup: if ( fComplete[0] || fComplete[1] ) // one of the cover is computed { vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL; - Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars ); + if ( iCube > 1 ) + Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars ); if ( fVeryVerbose ) { printf( "Processed output with %d supp vars and %d cubes.\n", nVars, Vec_StrSize(vRes)/(nVars +3) ); |