Version abc80517

1 files changed, 21 insertions, 11 deletions

diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index b8f93f57..ec6b7795 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -82,7 +82,7 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
     float TimeLeft = 0.0;
 
     // try the miter before solving
-    pNew = Aig_ManDup( p );
+    pNew = Aig_ManDupSimple( p );
     RetValue = Fra_FraigMiterStatus( pNew );
     if ( RetValue >= 0 )
         goto finish;
@@ -144,7 +144,7 @@ clk = clock();
 PRT( "Time", clock() - clk );
     }
     }
-    
+     
     // run latch correspondence
 clk = clock();
     if ( pNew->nRegs )
@@ -165,22 +165,27 @@ clk = clock();
         }
     }
     pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
+    p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+    Aig_ManStop( pTemp );
     if ( pNew == NULL )
     {
+        if ( p->pSeqModel )
+        {
+            RetValue = 0;
+            printf( "Networks are NOT EQUIVALENT after simulation.   " );
+PRT( "Time", clock() - clkTotal );
+            if ( pParSec->fReportSolution && !pParSec->fRecursive )
+            {
+            printf( "SOLUTION: FAIL       " );
+PRT( "Time", clock() - clkTotal );
+            }
+            return RetValue;
+        }
         pNew = pTemp;
         RetValue = -1;
         TimeOut = 1;
         goto finish;
     }
-    p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
-    Aig_ManStop( pTemp );
-    if ( pNew == NULL )
-    {
-        RetValue = 0;
-        printf( "Networks are NOT EQUIVALENT after simulation.   " );
-PRT( "Time", clock() - clkTotal );
-        return RetValue;
-    }
 
     if ( pParSec->fVerbose )
     {
@@ -354,6 +359,11 @@ PRT( "Time", clock() - clk );
             RetValue = 0;
             printf( "Networks are NOT EQUIVALENT after simulation.   " );
 PRT( "Time", clock() - clkTotal );
+            if ( pParSec->fReportSolution && !pParSec->fRecursive )
+            {
+            printf( "SOLUTION: FAIL       " );
+PRT( "Time", clock() - clkTotal );
+            }
             return RetValue;
         }
         Fra_SmlStop( pSml );