4 files changed, 25 insertions, 15 deletions

diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 3be0e3f6..df92792a 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -105,9 +105,9 @@ static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * p
     // set the new node
     Fra_ObjSetFraig( pObj, iFrame, pObjNew2 );
     // add the constraint
-    pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
-    pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
-    pMiter = Aig_Not( pMiter );
+    pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew );
+    pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
+    assert( Aig_ObjPhaseReal(pMiter) == 1 );
     Aig_ObjCreatePo( pManFraig, pMiter );
 }
 
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 );
diff --git a/src/aig/fra/fraSec80516.zip b/src/aig/fra/fraSec80516.zip
new file mode 100644
index 00000000..0adf10df
--- /dev/null
+++ b/src/aig/fra/fraSec80516.zip
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index b14dd5bd..a8de5e37 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -994,7 +994,7 @@ Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
     }
     return pCex;
 }
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Generates seq counter-example from the combinational one.]