Bug fix in &gla.

1 files changed, 12 insertions, 3 deletions

diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index dfe01a23..2b65170a 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/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));