diff options
| -rw-r--r-- | src/sat/bmc/bmcClp.c | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index d4a6cec7..956ccc7c 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -314,7 +314,10 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f { iLit = Vec_IntEntry( vLits, iVar ); Vec_IntPush( vCube, Abc_LitNot(iLit) ); - Vec_StrWriteEntry( vSop, Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) ); + if ( fReverse ) + Vec_StrWriteEntry( vSop, Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) ); + else + Vec_StrWriteEntry( vSop, Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) ); } if ( fVerbose ) printf( "Cube %4d: %s", Count, Vec_StrArray(vSop) + Start ); |