From c7e855619a1ea5997b68a235c27187a1b43252dc Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 24 Jan 2012 14:39:49 -0800
Subject: Variable timeframe abstraction.

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

(limited to 'src/aig/gia')

diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index e3baeb7b..4af2b7e7 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -939,8 +939,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
     // check the output
     if ( !Vta_ValIs1(pTop, Gia_ObjFaninC0(Gia_ManPo(p->pGia, 0))) )
         printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
-    else
-        printf( "Verification OK.\n" );
+//    else
+//        printf( "Verification OK.\n" );
 
     // produce true counter-example
     if ( pTop->Prio == 0 )
@@ -1285,6 +1285,7 @@ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
     int i, Entry;
     Vec_IntForEachEntry( vOne, Entry, i )
         Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
+    sat_solver2_simplify( p->pSat );
     printf( "\n\n" );
 }
 
-- 
cgit v1.2.3