From caf3e5a449dd665e2932b4f3eccdc042d977271e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Jul 2014 08:41:09 -0700 Subject: [PATCH] fix(kernel/metavar): missing justification bug Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 665777d343..c1e3efc43f 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -164,9 +164,9 @@ protected: } } else { if (m_update) { - expr r = m_subst.d_instantiate_metavars_wo_jst(p1->first); - m_subst.d_assign(m_name, r); - return r; + auto p2 = m_subst.d_instantiate_metavars(p1->first); + m_subst.d_assign(m_name, p2.first, mk_composite1(p1->second, p2.second)); + return p2.first; } else { return m_subst.instantiate(p1->first); }