From bea0d45e6ac64445009a5c00d3ddae4a0c60175b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 May 2020 09:38:17 -0700 Subject: [PATCH] disable new nlsat connection from master until debugged Signed-off-by: Nikolaj Bjorner --- 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 8f44a632a..c5403b66f 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 (ret == l_undef) { // disable the call to nlsat + if (false && ret == l_undef) { // disable the call to nlsat ret = run_nra(expl); if (ret == l_true || expl.size() > 0) { set_use_nra_model(true);