From cd87539de5b449d77da36f7555e9e927b9a555d3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Sep 2014 09:56:32 -0700 Subject: [PATCH] fix(library/unifier): bug in the new next_delta_unfold_case_split --- src/library/unifier.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 80a7f1799..e0506902e 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -1204,12 +1204,16 @@ struct unifier_fn { if (dcs.first) { constraints cnstrs = dcs.second.to_list(); return process_constraints(cnstrs, mk_composite1(cs.get_jst(), mk_assumption_justification(cs.m_assumption_idx))); + } else { + set_conflict(j); + return false; } + } else { + // update conflict + update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications)); + pop_case_split(); + return false; } - // update conflict - update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications)); - pop_case_split(); - return false; } /**