4 files changed, 9 insertions, 6 deletions
diff --git a/src/sat/bmc/bmcMesh.c b/src/sat/bmc/bmcMesh.c
index 6d85a6a1..6da70a1c 100644
--- a/src/sat/bmc/bmcMesh.c
+++ b/src/sat/bmc/bmcMesh.c
@@ -53,8 +53,9 @@ static inline int Bmc_MeshUVar( int Me[102][102], int x, int y ) { return Me[x][
 ***********************************************************************/
 static inline int Bmc_MeshVarValue( satoko_t * p, int v )
 {
-    int value = var_value(p, v) != VAR_UNASSING ? var_value(p, v) : var_polarity(p, v);
-    return value == LIT_TRUE;
+//    int value = var_value(p, v) != VAR_UNASSING ? var_value(p, v) : var_polarity(p, v);
+//    return value == LIT_TRUE;
+    return var_polarity(p, v) == LIT_TRUE;
 }
 
 /**Function*************************************************************
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 18d00ba2..368ece2f 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -518,9 +518,9 @@ void solver_cancel_until(solver_t *s, unsigned level)
     for (i = (int) vec_uint_size(s->trail) - 1; i >= (int) vec_uint_at(s->trail_lim, level); i--) {
         unsigned var = lit2var(vec_uint_at(s->trail, (unsigned) i));
 
+        vec_char_assign(s->polarity, var, vec_char_at(s->assigns, var));
         vec_char_assign(s->assigns, var, VAR_UNASSING);
         vec_uint_assign(s->reasons, var, UNDEF);
-        vec_char_assign(s->polarity, var, lit_polarity(vec_uint_at(s->trail, (unsigned) i)));
         if (!heap_in_heap(s->var_order, var))
             heap_insert(s->var_order, var);
     }
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
index 44bbaebd..94035d6e 100644
--- a/src/sat/satoko/solver.h
+++ b/src/sat/satoko/solver.h
@@ -207,6 +207,8 @@ static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason)
     unsigned var = lit2var(lit);
 
     vec_char_assign(s->assigns, var, lit_polarity(lit));
+    if ( solver_dlevel(s) == 0 )
+        vec_char_assign(s->polarity, var, lit_polarity(lit));
     vec_uint_assign(s->levels, var, solver_dlevel(s));
     vec_uint_assign(s->reasons, var, reason);
     vec_uint_push_back(s->trail, lit);
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 6b736731..f0aff0cc 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -480,9 +480,9 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
         return;
     }
     fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig);
-    array = vec_uint_data(s->trail);
-    for (i = 0; i < vec_uint_size(s->trail); i++)
-        fprintf(file, "%d\n", array[i] & 1 ? -(array[i] + !zero_var) : array[i] + !zero_var);
+    for (i = 0; i < vec_char_size(s->assigns); i++)
+        if ( var_value(s, i) != VAR_UNASSING )
+            fprintf(file, "%d\n", var_value(s, i) == LIT_FALSE ? -(int)(i + !zero_var) : i + !zero_var);
     
     array = vec_uint_data(s->originals);
     for (i = 0; i < vec_uint_size(s->originals); i++)