Skip to content

Commit

Permalink
fix #4163
Browse files Browse the repository at this point in the history
  • Loading branch information
NikolajBjorner committed May 1, 2020
1 parent cb5c2d3 commit 9757413
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/smt/dyn_ack.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -398,7 +398,7 @@ namespace smt {
}

literal dyn_ack_manager::mk_eq(expr * n1, expr * n2) {
app * eq = m_context.mk_eq_atom(n1, n2);
app_ref eq(m_context.mk_eq_atom(n1, n2), m);
m_context.internalize(eq, true);
literal l = m_context.get_literal(eq);
TRACE("dyn_ack", tout << "eq:\n" << mk_pp(eq, m) << "\nliteral: ";
Expand Down

0 comments on commit 9757413

Please sign in to comment.