Version abc80610

1 files changed, 11 insertions, 8 deletions

diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index e91478a4..d67839a4 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -53,19 +53,22 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
     // derive CNF
     pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
 //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
-    // convert into the SAT solver
+    // convert into SAT solver
     pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    // add the OR clause for the outputs
-    Cnf_DataWriteOrClause( pSat, pCnf );
-    vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
-    Cnf_DataFree( pCnf );
-    // solve SAT
     if ( pSat == NULL )
     {
-        Vec_IntFree( vCiIds );
-//        printf( "Trivially unsat\n" );
+        Cnf_DataFree( pCnf );
         return 1;
     }
+    // add the OR clause for the outputs
+    if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
+    {
+        sat_solver_delete( pSat );
+        Cnf_DataFree( pCnf );
+        return 1;
+    }
+    vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
+    Cnf_DataFree( pCnf );
 
 
 //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );