From 0f1624e5d218cda55a8526c9338f68b2122b86fd Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 28 Jul 2016 10:49:59 -0700
Subject: The same bug fix in 'scorr -c' (signal correspondence with
 constraints).

---
 src/proof/ssw/sswConstr.c | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index a9ed17fc..a3a7e66f 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -533,8 +533,10 @@ clk = Abc_Clock();
                 continue;
             }
             Ssw_NodesAreConstrained( p, pObjNew, Aig_ManConst0(p->pFrames) );
-        }
-
+        }        
+        // sweep flops
+        Saig_ManForEachLo( p->pAig, pObj, i )
+            p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 1 );
         // sweep internal nodes
         Aig_ManForEachNode( p->pAig, pObj, i )
         {
-- 
cgit v1.2.3