From d47d326cef8fd5de0cfbe4060bb8e752cad4fb4e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 Aug 2014 14:35:39 -0700 Subject: [PATCH] fix(library/unifier): bug in mk_imitiation_arg Remove bogus constraint cs.push_back(mk_eq_cnstr(mk_app(maux_type, locals), type, j, relax)); This constraint is incorrect because 'type' may contain local constants that are not in 'locals'. We just rely on cs.push_back(mk_eq_cnstr(mk_app(maux, margs), arg, j, relax)); When maux is assigned, the system will inforce that its type (which is based on maux_type) must be type correct Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 69a725b1c..dd807280f 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -1453,7 +1453,6 @@ struct unifier_fn { } else { expr maux_type = mk_metavar(u.m_ngen.next(), Pi(locals, mk_sort(mk_meta_univ(u.m_ngen.next())))); expr maux = mk_metavar(u.m_ngen.next(), Pi(locals, mk_app(maux_type, locals))); - cs.push_back(mk_eq_cnstr(mk_app(maux_type, locals), type, j, relax)); cs.push_back(mk_eq_cnstr(mk_app(maux, margs), arg, j, relax)); return mk_app(maux, locals); }