diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-16 19:45:25 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-16 19:45:25 -0700 |
| commit | 17cbe3567e1dc128610e8a714cc5ca702f4259f1 (patch) | |
| tree | 71e2347b6b0fd5a2aa91422119c55d0a02ed41db /src/sat | |
| parent | aa546b46d9051470e06457e820b0aa6f668c5bef (diff) | |
| download | abc-17cbe3567e1dc128610e8a714cc5ca702f4259f1.tar.gz abc-17cbe3567e1dc128610e8a714cc5ca702f4259f1.tar.bz2 abc-17cbe3567e1dc128610e8a714cc5ca702f4259f1.zip | |
Bug fix in 'satclp -r'.
Diffstat (limited to 'src/sat')
| -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 ); |