From 309ab1c12b262229d6d12071b3bee8d4ffc8b56f Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 11 Feb 2012 20:48:23 -0800
Subject: Variable timeframe abstraction.

---
 src/aig/gia/giaAbsVta.c | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'src/aig')

diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index fe5a8c36..21e31cd2 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -654,7 +654,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
     Gia_Obj_t * pObj;
     int i, Counter;
 
-//    Vta_ManSatVerify( p );
+    Vta_ManSatVerify( p );
 
     // collect nodes in a topological order
     vOrder = Vta_ManCollectNodes( p, f );
@@ -664,7 +664,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
         pThis->fVisit = 0;
     }
-/*
+
     // verify
     Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
     {
@@ -691,7 +691,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
             else assert( 0 );
         }
     }
-*/
+
     // compute distance in reverse order
     pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
     pThis->Prio  = 1;
@@ -883,7 +883,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
             assert( 0 );
     }
 
-/*
+
     // verify
     Vta_ManForEachObjVec( vOrder, p, pThis, i )
         pThis->Value = VTA_VARX;
@@ -948,7 +948,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
 //    else
 //        printf( "Verification OK.\n" );
-*/
+
 
     // produce true counter-example
     if ( pTop->Prio == 0 )
-- 
cgit v1.2.3