From 695231148faf8651b0299db234607cc545b962d3 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 31 Oct 2013 16:41:25 -0400
Subject: Specialized induction check.

---
 src/sat/bmc/bmcICheck.c | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'src/sat/bmc/bmcICheck.c')

diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c
index 61d42f29..d7048c21 100644
--- a/src/sat/bmc/bmcICheck.c
+++ b/src/sat/bmc/bmcICheck.c
@@ -170,6 +170,8 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos
         {
             iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj)];
             iVar1 = Vec_IntEntry( vLits, i );
+            if ( iVar1 == -1 )
+                continue;
             sat_solver_add_buffer( pSat, iVar0, iVar1, 0 );
         }
         // add equality clauses for the COs
@@ -204,6 +206,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos
     sat_solver_compress( pSat );
     while ( 1 )
     {
+//        sat_solver_bookmark( pSat );
         status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         if ( status == l_Undef )
         {
@@ -226,6 +229,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos
         if ( nLits == Vec_IntSize(vLits) )
             break;
         break;
+//        sat_solver_rollback( pSat );
 
         // add another large OR clause
         Vec_IntClear( vLits );
@@ -235,7 +239,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos
         // create new literals
         Vec_IntClear( vLits );
         for ( i = 0; i < nLits; i++ )
-            Vec_IntPush( vLits, pLits[i] );
+            Vec_IntPush( vLits, Abc_LitNot(pLits[i]) );
     }
 
     sat_solver_delete( pSat );
-- 
cgit v1.2.3