diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index d5703f50d..b3580abff 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -2238,9 +2238,6 @@ struct unifier_fn { postpone(c); return true; } - // The following condition is "dead-code" - if (!m_config.m_expensive_classes && cidx >= get_group_first_index(cnstr_group::ClassInstance)) - m_pattern = true; // use only higher-order (pattern) matching after we start processing class-instance constraints // std::cout << "process_next: " << c << "\n"; m_cnstrs.erase_min(); if (is_choice_cnstr(c)) {