Bug fix in &gla.

src/aig/gia/giaAbsGla2.c

@@ -1484,6 +1484,15 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             nVarsOld = p->nSatVars;
             for ( c = 0; ; c++ )
             {
+                // consider the special case when the target literal is implied false
+                // by implications which happened as a result of previous refinements
+                // note that incremental UNSAT core cannot be computed because there is no learned clauses
+                // in this case, we will assume that UNSAT core cannot reduce the problem
+                if ( var_is_assigned(p->pSat, Abc_Lit2Var(Lit)) )
+                {
+                    Prf_ManStopP( &p->pSat->pPrf2 );
+                    break;
+                }
                 // perform SAT solving
                 clk2 = clock();
                 Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );

src/sat/bsat/satProof2.h

@@ -290,6 +290,7 @@ static inline Vec_Int_t * Prf_ManUnsatCore( Prf_Man_t * p )
     int i, Entry;
     assert( p->iFirst >= 0 );
     assert( p->pInfo == NULL );
+    assert( Prf_ManSize(p) > 0 );
     vCore = Vec_IntAlloc( 64 * p->nWords );
     p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
     if ( p->vId2Pr == NULL )

src/sat/bsat/satSolver2.c

@@ -80,8 +80,9 @@ struct varinfo2_t
 //    unsigned lev    : 24;  // variable level
 };
 
-int    var_is_partA (sat_solver2* s, int v)              { return s->vi[v].partA;  }
-void   var_set_partA(sat_solver2* s, int v, int partA)   { s->vi[v].partA = partA; }
+int    var_is_assigned(sat_solver2* s, int v)            { return s->assigns[v] != varX; }
+int    var_is_partA (sat_solver2* s, int v)              { return s->vi[v].partA;        }
+void   var_set_partA(sat_solver2* s, int v, int partA)   { s->vi[v].partA = partA;       }
 
 //static inline int     var_level     (sat_solver2* s, int v)            { return s->vi[v].lev; }
 static inline int     var_level     (sat_solver2* s, int v)            { return s->levels[v];  }
@@ -95,6 +96,11 @@ static inline void    var_set_level (sat_solver2* s, int v, int lev)   { s->leve
 static inline void    var_set_value (sat_solver2* s, int v, int val)   { s->assigns[v] = val; }
 static inline void    var_set_polar (sat_solver2* s, int v, int pol)   { s->vi[v].pol = pol;  }
 
+// check if the literal is false under current assumptions
+static inline int     solver2_lit_is_false( sat_solver2* s, int Lit )  { return var_value(s, lit_var(Lit)) == !lit_sign(Lit); }
+
+
+
 // variable tags
 static inline int     var_tag       (sat_solver2* s, int v)            { return s->vi[v].tag; }
 static inline void    var_set_tag   (sat_solver2* s, int v, int tag)   {
@@ -1884,7 +1890,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
             }
             else
             {
-                assert( 0 );
+//                assert( 0 );
+//                r = var_unit_clause( s, lit_var(p) );
+//                assert( r != NULL );
+//                proof_id = clause2_proofid(s, r, 0);
                 proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions)
                 veci_resize(&s->conf_final,0);
                 veci_push(&s->conf_final, lit_neg(p));

src/sat/bsat/satSolver2.h

@@ -62,8 +62,9 @@ extern int *        Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars
 extern void         Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );
 
 // global variables
-extern int          var_is_partA (sat_solver2* s, int v);
-extern void         var_set_partA(sat_solver2* s, int v, int partA);
+extern int          var_is_assigned(sat_solver2* s, int v);
+extern int          var_is_partA   (sat_solver2* s, int v);
+extern void         var_set_partA  (sat_solver2* s, int v, int partA);
 
 // proof-based APIs
 extern void *       Sat_ProofCore( sat_solver2 * s );