summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2016-03-25 13:51:05 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2016-03-25 13:51:05 -0700
commit81b70c4d20ebe798a5440653ebd40e26bbe99f72 (patch)
tree70caca0ec4c4d76010e8cc1f175088c45ad7d610
parent72ffddb0add61ede9866e41382f2b6e126069e8d (diff)
downloadabc-81b70c4d20ebe798a5440653ebd40e26bbe99f72.tar.gz
abc-81b70c4d20ebe798a5440653ebd40e26bbe99f72.tar.bz2
abc-81b70c4d20ebe798a5440653ebd40e26bbe99f72.zip
Corner-case bug fix in 'satclp' with conflict limit.
-rw-r--r--src/sat/bmc/bmcClp.c15
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;
}
/*
{