diff options
Diffstat (limited to 'src/aig/gia/giaAbsVta.c')
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 735bb823..f7c1e5a5 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1528,6 +1528,19 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // preconditions assert( Gia_ManPoNum(pAig) == 1 ); assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); + if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) ) + { + if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) ) + { + printf( "Sequential miter is trivially UNSAT.\n" ); + return 1; + } + ABC_FREE( pAig->pCexSeq ); + pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 ); + printf( "Sequential miter is trivially SAT.\n" ); + return 0; + } + // compute intial abstraction if ( pAig->vObjClasses == NULL ) { |