summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2015-04-17 11:04:14 +0900
committerAlan Mishchenko <alanmi@berkeley.edu>2015-04-17 11:04:14 +0900
commitb1aabead5d5d73a040f9fcbd0526febc61820176 (patch)
treebe17b287a07db4bb7f649caa2b83fe658908847f /src/sat
parentcd4807ea043b6179b22bdb281318e8d3b6911c8b (diff)
downloadabc-b1aabead5d5d73a040f9fcbd0526febc61820176.tar.gz
abc-b1aabead5d5d73a040f9fcbd0526febc61820176.tar.bz2
abc-b1aabead5d5d73a040f9fcbd0526febc61820176.zip
Bug fix in &satfx.
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bmc/bmcFx.c4
1 files changed, 2 insertions, 2 deletions
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 );