fix #4163

NikolajBjorner · NikolajBjorner · commit 97574134e0b5 · 2020-04-30T19:30:40.000-07:00
diff --git 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: "; 

Original file line number	Diff line number	Diff line change
`@@ -398,7 +398,7 @@ namespace smt {`
`398`	`398`	`}`
`399`	`399`
`400`	`400`	`literal dyn_ack_manager::mk_eq(expr * n1, expr * n2) {`
`401`		`- app * eq = m_context.mk_eq_atom(n1, n2);`
	`401`	`+ app_ref eq(m_context.mk_eq_atom(n1, n2), m);`
`402`	`402`	`m_context.internalize(eq, true);`
`403`	`403`	`literal l = m_context.get_literal(eq);`
`404`	`404`	`TRACE("dyn_ack", tout << "eq:\n" << mk_pp(eq, m) << "\nliteral: ";`