1 files changed, 8 insertions, 8 deletions
diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c
index fa52e2b6..dcc80b29 100644
--- a/src/aig/int/intContain.c
+++ b/src/aig/int/intContain.c
@@ -200,19 +200,19 @@ int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter,
     assert( Vec_PtrSize(vMapRegs) == (nSteps + 1) * nRegs );
     // add main constraints to the timeframes
     ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs);
-    if ( fBackward )
-    {
-        // p -> !p -> ... -> !p
-        Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 );
-        for ( f = 1; f <= nSteps; f++ )
+    if ( !fBackward )
+    { 
+        // forward inductive check: p -> p -> ... -> !p
+        for ( f = 0; f < nSteps; f++ )
             Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
+        Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 );
     }
     else
     {
-        // !p -> p -> ... -> p
-        for ( f = 0; f < nSteps; f++ )
+        // backward inductive check: p -> !p -> ... -> !p
+        Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 );
+        for ( f = 1; f <= nSteps; f++ )
             Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
-        Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 );
     }
     Vec_PtrFree( vMapRegs );
     Aig_ManCleanup( pFrames );