From 5be1893d9865735d91ee082360419654025f68ed Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Nov 2015 16:38:44 -0800 Subject: [PATCH] fix(library/blast/state): bug at instantiate_urefs_mrefs --- src/library/blast/state.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 98183cecb..a3dd6d662 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -292,7 +292,7 @@ struct instantiate_urefs_mrefs_fn : public replace_visitor { } virtual expr visit(expr const & e) { - if (!has_mref(e) || !has_univ_metavar(e)) + if (!has_mref(e) && !has_univ_metavar(e)) return e; else return replace_visitor::visit(e);