From e7a5a74b4c2c83add24fa60ea8c88977c0e4ca69 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 25 Jul 2011 20:35:06 +0700
Subject: Adding procedures to find the care bits of a counter-example.

---
 src/base/abci/abc.c | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'src/base/abci')

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1bd53dea..6058998e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8763,20 +8763,19 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Aig_ManStop( pAig );
 }
 */
-/*
+
 {
     extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-    extern Abc_Cex_t * Saig_PhaseTranslateCex( Aig_Man_t * p, Abc_Cex_t * pCex );
     if ( pAbc->pCex && pNtk )
     {
         Abc_Cex_t * pNew;
         Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        pNew = Saig_PhaseTranslateCex( pAig, pAbc->pCex );
+        pNew = Saig_ManRefineCexSat( pAig, pAbc->pCex, 0, 0 );
         Aig_ManStop( pAig );
         Abc_FrameReplaceCex( pAbc, &pNew );
     }
 }
-*/
+
 
     return 0;
 usage:
-- 
cgit v1.2.3