diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index f083c0f82..e131cc2be 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -231,14 +231,12 @@ struct solver::imp {
                 if (!check_constraint(ci)) {
                     IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n";
                                lra.constraints().display(verbose_stream()));
-                    UNREACHABLE();
                     return l_undef;
                 }
             for (auto const &m : m_nla_core.emons()) {
                 if (!check_monic(m)) {
                     IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n";
                                lra.constraints().display(verbose_stream()));
-                    UNREACHABLE();
                     return l_undef;
                 }
             }