Bug fix in &satfx.

b1aabead · Alan Mishchenko · cd4807ea · b1aabead
Commit b1aabead authored Apr 17, 2015 by Alan Mishchenko
Show whitespace changes
Inline Side-by-side

Showing with 2 additions and 2 deletions

src/sat/bmc/bmcFx.c
+2 -2

No files found.
--- 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 );