From 97574134e0b57e2ff382a2810e6e52400e220248 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Apr 2020 19:30:40 -0700 Subject: [PATCH] fix #4163 --- src/smt/dyn_ack.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index 2fe547cf7..dc0ae2551 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -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: ";