From a14c2a30516003cd1a60f8b7deca029033d11c78 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 11 May 2020 17:39:30 -0700 Subject: [PATCH] enable nlsat solver call from nla Signed-off-by: Lev Nachmanson --- src/math/lp/nla_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index c5403b66f..8f44a632a 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -34,7 +34,7 @@ lbool solver::run_nra(lp::explanation & expl) { lbool solver::check(vector& l, lp::explanation& expl) { set_use_nra_model(false); lbool ret = m_core->check(l); - if (false && ret == l_undef) { // disable the call to nlsat + if (ret == l_undef) { // disable the call to nlsat ret = run_nra(expl); if (ret == l_true || expl.size() > 0) { set_use_nra_model(true);