From 50e21586b0129690d32a4e3b82c083ad66726dcc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Jun 2014 18:52:13 -0700 Subject: [PATCH] feat(library/unifier): do not create a case-split for choice constraints that produce only one alternative Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 1b046a8354..b685e7a818 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -799,9 +799,14 @@ struct unifier_fn { auto r = rlist.pull(); justification j = mk_composite1(c.get_justification(), m_type_jst.second); if (r) { - justification a = mk_assumption_justification(m_next_assumption_idx); - add_case_split(std::unique_ptr(new choice_case_split(*this, m, m_type_jst.second, r->second))); - return process_choice_result(m, r->first, mk_composite1(j, a)); + if (r->second.is_nil()) { + // there is only one alternative + return process_choice_result(m, r->first, j); + } else { + justification a = mk_assumption_justification(m_next_assumption_idx); + add_case_split(std::unique_ptr(new choice_case_split(*this, m, m_type_jst.second, r->second))); + return process_choice_result(m, r->first, mk_composite1(j, a)); + } } else { set_conflict(j); return false;