diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index b368fdfec..85a55cd6b 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -404,7 +404,7 @@ struct solver::imp { lemma |= inq; } IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); - m_nla_core.set_use_nra_model(true); + //m_nla_core.set_use_nra_model(true); return l_false; }