Commit 1d44f420 by Alan Mishchenko

Change in Satoko to make assumption var values appear in satisfiable assignments produced.

parent f9914988
......@@ -290,6 +290,7 @@ void satoko_assump_push(solver_t *s, int lit)
assert(lit2var(lit) < satoko_varnum(s));
// printf("[Satoko] Push assumption: %d\n", lit);
vec_uint_push_back(s->assumptions, lit);
vec_char_assign(s->polarity, lit2var(lit), lit_polarity(lit));
}
void satoko_assump_pop(solver_t *s)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment