diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-24 14:39:49 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-24 14:39:49 -0800 |
| commit | c7e855619a1ea5997b68a235c27187a1b43252dc (patch) | |
| tree | 1686518e526d31e49496533b034beff9b029e3e8 /src/aig | |
| parent | 94d35a2592911d732d20a6ae9c2b3c6e75b83fa3 (diff) | |
| download | abc-c7e855619a1ea5997b68a235c27187a1b43252dc.tar.gz abc-c7e855619a1ea5997b68a235c27187a1b43252dc.tar.bz2 abc-c7e855619a1ea5997b68a235c27187a1b43252dc.zip | |
Variable timeframe abstraction.
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 5 |
1 files changed, 3 insertions, 2 deletions
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" ); } |