Several corner-case bug fixes in scorr with constraints.

src/base/abci/abc.c

@@ -21211,10 +21211,18 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( pPars->fConstrs )
     {
+        if ( Abc_NtkConstrNum(pNtk) == Abc_NtkPoNum(pNtk) )
+        {
+            Abc_Print( 0, "Command cannot be applied because the network has only constraint outputs (no primary outputs).\n" );
+            return 0;
+        }
         if ( Abc_NtkConstrNum(pNtk) > 0 )
             Abc_Print( 0, "Performing scorr with %d constraints.\n", Abc_NtkConstrNum(pNtk) );
         else
+        {
             Abc_Print( 0, "Performing constraint-based scorr without constraints.\n" );
+            pPars->fConstrs = 0;
+        }
     }
     if ( pPars->fEquivDump && pPars->fEquivDump2 )
     {

src/proof/ssw/sswCore.c

@@ -496,7 +496,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
         Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
     }
     // allocate storage
-    if ( p->pPars->fLocalSim )
+    if ( p->pPars->fLocalSim && p->pSml )
         p->pVisited = ABC_CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) );
     // perform refinement of classes
     pAigNew = Ssw_SignalCorrespondenceRefine( p );