From b1aabead5d5d73a040f9fcbd0526febc61820176 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 17 Apr 2015 11:04:14 +0900 Subject: Bug fix in &satfx. --- src/sat/bmc/bmcFx.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bmc/bmcFx.c b/src/sat/bmc/bmcFx.c index 09517c26..9cd37c88 100644 --- a/src/sat/bmc/bmcFx.c +++ b/src/sat/bmc/bmcFx.c @@ -553,9 +553,9 @@ int Bmc_FxSolve( sat_solver * pSat, int iOut, int iAuxVar, Vec_Int_t * vVars, in assert( iVar >= 0 && iVar < Vec_IntSize(vVars) ); //printf( "%s%d ", Abc_LitIsCompl(pFinal[i]) ? "+":"-", iVar ); if ( fDumpPla ) - Vec_StrWriteEntry( vCube, iVar, (char)(Abc_LitIsCompl(pFinal[i]) ? '0' : '1') ); + Vec_StrWriteEntry( vCube, iVar, (char)(!Abc_LitIsCompl(pFinal[i]) ? '0' : '1') ); if ( vLevel ) - Vec_IntPush( vLevel, Abc_Var2Lit(iVar, Abc_LitIsCompl(pFinal[i])) ); + Vec_IntPush( vLevel, Abc_Var2Lit(iVar, !Abc_LitIsCompl(pFinal[i])) ); } if ( vCubes ) Vec_IntSort( vLevel, 0 ); -- cgit v1.2.3