diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-03-25 13:51:05 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-03-25 13:51:05 -0700 |
| commit | 81b70c4d20ebe798a5440653ebd40e26bbe99f72 (patch) | |
| tree | 70caca0ec4c4d76010e8cc1f175088c45ad7d610 /src | |
| parent | 72ffddb0add61ede9866e41382f2b6e126069e8d (diff) | |
| download | abc-81b70c4d20ebe798a5440653ebd40e26bbe99f72.tar.gz abc-81b70c4d20ebe798a5440653ebd40e26bbe99f72.tar.bz2 abc-81b70c4d20ebe798a5440653ebd40e26bbe99f72.zip | |
Corner-case bug fix in 'satclp' with conflict limit.
Diffstat (limited to 'src')
| -rw-r--r-- | src/sat/bmc/bmcClp.c | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index 41080662..eb924123 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -459,12 +459,15 @@ int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLit if ( k == nFinal ) Vec_IntWriteEntry( vLits, i, -1 ); } - Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, fOnOffSetLit ); + if ( Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, fOnOffSetLit ) == -1 ) + return -1; } else { - Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ); - Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ); + if ( Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ) == -1 ) + return -1; + if ( Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ) == -1 ) + return -1; } { // put into new array @@ -559,8 +562,10 @@ int Bmc_CollapseExpand2( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLi } else { - Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ); - Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ); + if ( Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ) == -1 ) + return -1; + if ( Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ) == -1 ) + return -1; } /* { |