From a2d59be3f7f05c4757ade8b3b6f9fdf425de5cc0 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 25 Mar 2018 18:19:06 -0700
Subject: Integrating SAT-based CEX minimization (bug fix).

---
 src/sat/bmc/bmcCexCare.c | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'src/sat')

diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c
index 8db92444..c274b04c 100644
--- a/src/sat/bmc/bmcCexCare.c
+++ b/src/sat/bmc/bmcCexCare.c
@@ -439,11 +439,7 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t
         Gia_ManStop( pGia );
         return NULL;
     }
-    // verify and return
-    if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) )
-        printf( "Counter-example verification has failed.\n" );
-    else if ( fCheck ) 
-        printf( "Counter-example verification succeeded.\n" );
+    // unfortunately, cannot verify - ternary simulation does not work
     Gia_ManStop( pGia );
     return pCexMin;
 }
-- 
cgit v1.2.3