mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix bug exposed by lia2maxsmt4
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ddb30c51b5
commit
f0ef339623
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue