From f0ef339623e9f2738452d7f3e48e4341e2ba9fcf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Dec 2013 12:30:52 -0800 Subject: [PATCH] fix bug exposed by lia2maxsmt4 Signed-off-by: Nikolaj Bjorner --- src/opt/weighted_maxsat.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index dbc943fbd..48c25e4d5 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -87,6 +87,12 @@ namespace smt { SASSERT(v == m_var2bool.size()); m_var2bool.push_back(bv); SASSERT(ctx.bool_var2enode(bv)); + + lbool asgn = ctx.get_assignment(bv); + if (asgn == l_true) { + assign_eh(bv, true); + } + } if (m_min_cost_atom) { app* var = m_min_cost_atom;