From 6da21b8b884632c901ae10955e23c0c8206e7e58 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 5 Mar 2015 23:00:30 -0800
Subject: Experiments with SAT-based cube enumeration.

---
 src/sat/bmc/bmcEco.c | 6 ------
 1 file changed, 6 deletions(-)

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

diff --git a/src/sat/bmc/bmcEco.c b/src/sat/bmc/bmcEco.c
index c4fc3ba8..07fdd704 100644
--- a/src/sat/bmc/bmcEco.c
+++ b/src/sat/bmc/bmcEco.c
@@ -138,7 +138,6 @@ static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
 int Bmc_EcoSolve( sat_solver * pSat, int Root, Vec_Int_t * vVars )
 {
     int nBTLimit = 1000000;
-    Vec_Int_t * vValues = Vec_IntAlloc( Vec_IntSize(vVars) );
     Vec_Int_t * vLits   = Vec_IntAlloc( Vec_IntSize(vVars) );
     int status, i, Div, iVar, nFinal, * pFinal, nIter = 0, RetValue = 0;
     int pLits[2], nVars = sat_solver_nvars( pSat );
@@ -154,10 +153,6 @@ int Bmc_EcoSolve( sat_solver * pSat, int Root, Vec_Int_t * vVars )
         if ( status == l_False )
             { RetValue = 1; break; }
         assert( status == l_True );
-        // remember variable values
-        Vec_IntClear( vValues );
-        Vec_IntForEachEntry( vVars, iVar, i )
-            Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
         // collect divisor literals
         Vec_IntClear( vLits );
         Vec_IntPush( vLits, Abc_LitNot(pLits[0]) ); // F = 0
@@ -189,7 +184,6 @@ int Bmc_EcoSolve( sat_solver * pSat, int Root, Vec_Int_t * vVars )
         nIter++;
     }
 //    assert( status == l_True );
-    Vec_IntFree( vValues );
     Vec_IntFree( vLits );
     return RetValue;
 }
-- 
cgit v1.2.3