From 22fd7dca452be1c996436c5e5faa673ceff5ac96 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 4 Nov 2013 16:20:31 -0800
Subject: Specialized inductive check.

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

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

diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c
index 4376c336..17408e78 100644
--- a/src/sat/bmc/bmcICheck.c
+++ b/src/sat/bmc/bmcICheck.c
@@ -94,6 +94,7 @@ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pC
     Vec_Int_t * vLits;
     Gia_Obj_t * pObj, * pObj0, * pObj1;
     int i, k, iVar0, iVar1, iVarOut;
+    int VarShift = 0;
 
     // start the SAT solver
     pSat = sat_solver_new();
@@ -108,6 +109,8 @@ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pC
 
     // load the last timeframe
     Cnf_DataLiftGia( pCnf, pMiter, Gia_ManRegNum(p) + Gia_ManCoNum(p) );
+    VarShift += Gia_ManRegNum(p) + Gia_ManCoNum(p);
+
     // add XOR clauses
     Gia_ManForEachPo( p, pObj, i )
     {
@@ -141,6 +144,7 @@ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pC
             Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pMiter, pObj)] );
         // lift CNF again
         Cnf_DataLiftGia( pCnf, pMiter, pCnf->nVars );
+        VarShift += pCnf->nVars;
         // stitch the clauses
         Gia_ManForEachRi( pMiter, pObj, i )
         {
@@ -173,6 +177,7 @@ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pC
                 assert( 0 );
     }
 //    sat_solver_compress( pSat );
+    Cnf_DataLiftGia( pCnf, pMiter, -VarShift );
     Vec_IntFree( vLits );
     return pSat;
 }
-- 
cgit v1.2.3