Version abc70209

2 files changed, 12 insertions, 1 deletions

diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index e56c58f3..99942a88 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -179,7 +179,8 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
     // consider the case when cube pairs should be preprocessed
     // before adding them to the set of divisors
     if ( nPairsTotal > pData->nPairsMax )
-        Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax );
+        if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) )
+            return NULL;
 
     // add the var pairs to the heap
     Fxu_MatrixComputeSingles( p );
diff --git a/src/opt/fxu/fxuReduce.c b/src/opt/fxu/fxuReduce.c
index 3f3bc8fc..0ab8a157 100644
--- a/src/opt/fxu/fxuReduce.c
+++ b/src/opt/fxu/fxuReduce.c
@@ -90,6 +90,16 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
         pnPairCounters[ pnLitsDiff[k] ]++;
     // determine what pairs to take starting from the lower
     // so that there would be exactly pPairsMax pairs
+    if ( pnPairCounters[0] != 0 )
+    {
+        printf( "The SOPs of the nodes are not cube-free. Run \"bdd; sop\" before \"fx\".\n" );
+        return 0;
+    }
+    if ( pnPairCounters[1] != 0 )
+    {
+        printf( "The SOPs of the nodes are not SCC-free. Run \"bdd; sop\" before \"fx\".\n" );
+        return 0;
+    }
     assert( pnPairCounters[0] == 0 ); // otherwise, covers are not dup-free
     assert( pnPairCounters[1] == 0 ); // otherwise, covers are not SCC-free
     nSum = 0;