From a5698a55ec7b4dae43ab24fb2a63c4a0badda003 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Sep 2014 08:43:16 -0700 Subject: [PATCH] fix(library/unifier): catch type error when checking is_def_eq of type incorrect expressions --- src/library/unifier.cpp | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 7256e9a3d0..0de3ecebe9 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -485,13 +485,18 @@ struct unifier_fn { \remark If relax is true then opaque definitions from the main module are treated as transparent. */ bool is_def_eq(expr const & t1, expr const & t2, justification const & j, bool relax) { - auto dcs = m_tc[relax]->is_def_eq(t1, t2, j); - if (!dcs.first) { - // std::cout << "conflict: " << t1 << " =?= " << t2 << "\n"; + try { + auto dcs = m_tc[relax]->is_def_eq(t1, t2, j); + if (!dcs.first) { + // std::cout << "conflict: " << t1 << " =?= " << t2 << "\n"; + set_conflict(j); + return false; + } else { + return process_constraints(dcs.second); + } + } catch (exception&) { set_conflict(j); return false; - } else { - return process_constraints(dcs.second); } }