From 17cbe3567e1dc128610e8a714cc5ca702f4259f1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 16 Oct 2015 19:45:25 -0700 Subject: Bug fix in 'satclp -r'. --- src/sat/bmc/bmcClp.c | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'src') 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 ); -- cgit v1.2.3