From 1d44f420392d40a71c907a0ad7636983f2441f30 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 3 Sep 2017 07:28:04 -0700
Subject: Change in Satoko to make assumption var values appear in satisfiable
 assignments produced.

---
 src/sat/satoko/solver_api.c | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src')

diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 837d64e7..20217e54 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -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)
-- 
cgit v1.2.3