From 18a883ab1b990f0c403cdddf6693e573a235224a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Jun 2014 09:33:34 -0700 Subject: [PATCH] fix(library/unifier): set conflict if type mismatch during metavariable assignment Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 79ed0ec7a..bf546cc1d 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -457,8 +457,12 @@ struct unifier_fn { m_subst = m_subst.assign(m, v, j); expr m_type = mlocal_type(m); expr v_type = m_tc.infer(v); - if (in_conflict() || !m_tc.is_def_eq(m_type, v_type, j)) + if (in_conflict()) return false; + if (!m_tc.is_def_eq(m_type, v_type, j)) { + set_conflict(j); + return false; + } auto it = m_mvar_occs.find(mlocal_name(m)); if (it) { cnstr_idx_set s = *it;