Bug fix in interpolation (false positive if property fails in frame 0).

src/aig/int/intCore.c

@@ -93,12 +93,14 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
     assert( Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) == 1 );
     if ( pPars->fVerbose && Saig_ManConstrNum(pAig) )
         printf( "Performing interpolation with %d constraints...\n", Saig_ManConstrNum(pAig) );
-/*
+
     if ( Inter_ManCheckInitialState(pAig) )
     {
+        *piFrame = 0;
         printf( "Property trivially fails in the initial state.\n" );
         return 0;
     }
+/*
     if ( Inter_ManCheckAllStates(pAig) )
     {
         printf( "Property trivially holds in all states.\n" );

src/aig/int/intUtil.c

@@ -46,17 +46,28 @@ ABC_NAMESPACE_IMPL_START
 int Inter_ManCheckInitialState( Aig_Man_t * p )
 {
     Cnf_Dat_t * pCnf;
+    Aig_Obj_t * pObj;
     sat_solver * pSat;
-    int status;
+    int i, status;
     int clk = clock();
     pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 1 );
-    Cnf_DataFree( pCnf );
     if ( pSat == NULL )
+    {
+        Cnf_DataFree( pCnf );
         return 0;
+    }
     status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    sat_solver_delete( pSat );
     ABC_PRT( "Time", clock() - clk );
+    if ( status == l_True )
+    {
+        p->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), 1 );
+        Saig_ManForEachPi( p, pObj, i )
+            if ( sat_solver_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pObj)] ) )
+                Aig_InfoSetBit( p->pSeqModel->pData, Aig_ManRegNum(p) + i );
+    }
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
     return status == l_True;
 }