From f177c8d1ecc57b3b0d11efc3bf9f7dde32fe9d65 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2014 14:11:33 -0800 Subject: [PATCH] fix(library/elaborator): missing condition The elaborator was failing in the following higher-order constraint ctx |- (?M a) = (?M b) This constraint has solution, but the missing condition was making the elaborator to reduce this problem to ctx |- a = b That does not have a solution. Signed-off-by: Leonardo de Moura --- src/library/elaborator/elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 43f157a75..f888c5bfd 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -1354,7 +1354,7 @@ class elaborator::imp { if (process_assigned_metavar(c, a, true) || process_assigned_metavar(c, b, false)) return true; - if (m_assume_injectivity && is_app(a) && is_app(b) && num_args(a) == num_args(b) && arg(a, 0) == arg(b, 0)) { + if (m_assume_injectivity && is_app(a) && is_app(b) && num_args(a) == num_args(b) && arg(a, 0) == arg(b, 0) && !is_metavar(arg(a, 0))) { // If m_assume_injectivity is true, we apply the following rule // ctx |- (f a1 a2) == (f b1 b2) // ===>