3 files changed, 18 insertions, 17 deletions

diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h
index c40e5f18..0b1756ff 100644
--- a/src/sat/bsat/satClause.h
+++ b/src/sat/bsat/satClause.h
@@ -113,15 +113,15 @@ static inline double    Sat_MemMemoryAll( Sat_Mem_t * p )            { return 1.
 // i is page number
 // k is page offset
 
-// print problelm clauses NOT in proof mode
+// print problem clauses NOT in proof mode
 #define Sat_MemForEachClause( p, c, i, k )      \
     for ( i = 0; i <= p->iPage[0]; i += 2 )     \
-        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
+        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) ) if ( i == 0 && k == 2 ) {} else
 
-// print problem clauses in proof model
+// print problem clauses in proof mode
 #define Sat_MemForEachClause2( p, c, i, k )      \
     for ( i = 0; i <= p->iPage[0]; i += 2 )     \
-        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize2(c) )
+        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize2(c) ) if ( i == 0 && k == 2 ) {} else
 
 #define Sat_MemForEachLearned( p, c, i, k )     \
     for ( i = 1; i <= p->iPage[1]; i += 2 )     \
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 0e5c6b91..ab1203ea 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -401,6 +401,7 @@ static inline int sat_clause_compute_lbd( sat_solver* s, clause* c )
  */
 static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
 {
+    int fUseBinaryClauses = 1;
     int size;
     clause* c;
     int h;
@@ -410,7 +411,7 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
     size           = end - begin;
 
     // do not allocate memory for the two-literal problem clause
-    if ( size == 2 && !learnt )
+    if ( fUseBinaryClauses && size == 2 && !learnt )
     {
         veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1])));
         veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0])));
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 59eb047d..dc431440 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -78,7 +78,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin,
     // count the number of unit clauses
     nUnits = 0;
     for ( i = 0; i < p->size; i++ )
-        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+        if ( p->levels[i] == 0 && p->assigns[i] != 3 )
             nUnits++;
 
     // start the file
@@ -89,21 +89,21 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin,
         return;
     }
 //    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
-    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
+    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)-1+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
 
     // write the original clauses
     Sat_MemForEachClause( pMem, c, i, k )
         Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
     // write the learned clauses
-    Sat_MemForEachLearned( pMem, c, i, k )
-        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
+//    Sat_MemForEachLearned( pMem, c, i, k )
+//        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
     // write zero-level assertions
     for ( i = 0; i < p->size; i++ )
-        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+        if ( p->levels[i] == 0 && p->assigns[i] != 3 ) // varX
             fprintf( pFile, "%s%d%s\n",
-                     (p->assigns[i] == l_False)? "-": "",
+                     (p->assigns[i] == 1)? "-": "",    // var0
                      i + (int)(incrementVars>0),
                      (incrementVars) ? " 0" : "");
 
@@ -130,7 +130,7 @@ void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin
     // count the number of unit clauses
     nUnits = 0;
     for ( i = 0; i < p->size; i++ )
-        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+        if ( p->levels[i] == 0 && p->assigns[i] != 3 )
             nUnits++;
 
     // start the file
@@ -141,21 +141,21 @@ void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin
         return;
     }
 //    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
-    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
+    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)-1+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
 
     // write the original clauses
     Sat_MemForEachClause2( pMem, c, i, k )
         Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
     // write the learned clauses
-    Sat_MemForEachLearned( pMem, c, i, k )
-        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
+//    Sat_MemForEachLearned( pMem, c, i, k )
+//        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
     // write zero-level assertions
     for ( i = 0; i < p->size; i++ )
-        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+        if ( p->levels[i] == 0 && p->assigns[i] != 3 ) // varX
             fprintf( pFile, "%s%d%s\n",
-                     (p->assigns[i] == l_False)? "-": "",
+                     (p->assigns[i] == 1)? "-": "",    // var0
                      i + (int)(incrementVars>0),
                      (incrementVars) ? " 0" : "");