From 4c9723e5ed30e00b12372475b543549f04242a21 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Aug 2014 09:07:34 -0700 Subject: [PATCH] fix(library/unifier): assertion violation Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index ac73c5d78..f901d1943 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -1735,10 +1735,15 @@ struct unifier_fn { if (!all_local(lhs)) { expr rhs_whnf = whnf(rhs, j, relax, aux); if (rhs_whnf != rhs) { - buffer alts2; - process_flex_rigid_core(lhs, rhs_whnf, j, relax, alts2); - append_auxiliary_constraints(alts2, to_list(aux.begin(), aux.end())); - alts.append(alts2); + if (is_meta(rhs_whnf)) { + // it become a flex-flex constraint + alts.push_back(constraints(mk_eq_cnstr(lhs, rhs_whnf, j, relax))); + } else { + buffer alts2; + process_flex_rigid_core(lhs, rhs_whnf, j, relax, alts2); + append_auxiliary_constraints(alts2, to_list(aux.begin(), aux.end())); + alts.append(alts2); + } } }