Several small changes and fixes.

3 files changed, 11 insertions, 5 deletions

diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 680b1996..eeadf09e 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -396,11 +396,15 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
         if ( pNode->Id == 0 ) 
             continue;
         pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts );
+        assert( pNode->Id > 0 );
         Vec_PtrPush( vUsed, pNode );
         // update fanins
         Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
             if ( (pNode->pEnts[k] & 1) == 0 ) // proof node
+            {
+                assert( pFanin->Id > 0 );
                 pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2);
+            }
 //            else // problem clause
 //                assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) );
     }
@@ -420,7 +424,6 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
         if ( pPivot && pPivot <= pNode )
         {
             RetValue = hTemp;
-//            s->iProofPivot = i;
             pPivot = NULL;
         }
     }
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 520e8284..eace9eea 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -30,7 +30,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "satVec.h"
 #include "satClause.h"
-#include "misc/vec/vecSet.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index cb6199ec..2cd825b7 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -164,7 +164,7 @@ static inline void proof_chain_start( sat_solver2* s, clause* c )
     if ( s->fProofLogging )
     {
         int ProofId = clause2_proofid(s, c, 0);
-        assert( ProofId > 0 );
+        assert( (ProofId >> 2) > 0 );
         veci_resize( &s->temp_proof, 0 );
         veci_push( &s->temp_proof, 0 );
         veci_push( &s->temp_proof, 0 );
@@ -178,7 +178,7 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
     {
         clause* c = cls ? cls : var_unit_clause( s, Var );
         int ProofId = clause2_proofid(s, c, var_is_partA(s,Var));
-        assert( ProofId > 0 );
+        assert( (ProofId >> 2) > 0 );
         veci_push( &s->temp_proof, ProofId );
     }
 }
@@ -1417,7 +1417,10 @@ void sat_solver2_reducedb(sat_solver2* s)
             break;
     }
     if ( j < nLearnedOld / 6 )
+    {
+        ABC_FREE( pSortValues );
         return;
+    }
 
     // mark learned clauses to remove
     Counter = j = 0;
@@ -1439,6 +1442,7 @@ void sat_solver2_reducedb(sat_solver2* s)
             s->stats.learnts--;
         }
     }
+    ABC_FREE( pSortValues );
 //    if ( j == nLearnedOld )
 //        return;
 
@@ -1717,6 +1721,7 @@ void sat_solver2_verify( sat_solver2* s )
 //        Abc_Print(1, "Verification passed.\n" );
 }
 */
+
 // checks how many watched clauses are satisfied by 0-level assignments
 // (this procedure may be called before setting up a new bookmark for rollback)
 int sat_solver2_check_watched( sat_solver2* s )
@@ -1754,7 +1759,6 @@ int sat_solver2_check_watched( sat_solver2* s )
     return 0;
 }
 
-
 int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
 {
     int restart_iter = 0;