diff --git a/src/nlsat/nlsat_types.h b/src/nlsat/nlsat_types.h index b8c705891..11e063a17 100644 --- a/src/nlsat/nlsat_types.h +++ b/src/nlsat/nlsat_types.h @@ -113,14 +113,14 @@ namespace nlsat { inline std::ostream& operator<<(std::ostream& out, atom::kind k) { switch (k) { - case atom::kind::EQ: return out << "="; - case atom::kind::LT: return out << "<"; - case atom::kind::GT: return out << ">"; - case atom::kind::ROOT_EQ: return out << "= root"; - case atom::kind::ROOT_LT: return out << "< root"; - case atom::kind::ROOT_LE: return out << "<= root"; - case atom::kind::ROOT_GT: return out << "> root"; - case atom::kind::ROOT_GE: return out << ">= root"; + case atom::EQ: return out << "="; + case atom::LT: return out << "<"; + case atom::GT: return out << ">"; + case atom::ROOT_EQ: return out << "= root"; + case atom::ROOT_LT: return out << "< root"; + case atom::ROOT_LE: return out << "<= root"; + case atom::ROOT_GT: return out << "> root"; + case atom::ROOT_GE: return out << ">= root"; default: return out << (int)k; } return out; diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 75cf57fa3..b080b71a2 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -520,6 +520,7 @@ namespace qe { { m_smtp.m_model = true; m_smtp.m_relevancy_lvl = 0; + m_smtp.m_case_split_strategy = CS_ACTIVITY_WITH_CACHE; } smt::kernel& k() { return m_kernel; }