From 08940cff8f688fb5044388f23ae89b1ca4fec67f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 15 May 2020 11:26:40 -0700 Subject: [PATCH] comment out the call to nra_solver Signed-off-by: Lev Nachmanson --- configure | 0 contrib/ci/scripts/build_z3_cmake.sh | 0 contrib/ci/scripts/install_deps_osx.sh | 0 contrib/ci/scripts/test_z3_docs.sh | 0 contrib/ci/scripts/test_z3_examples_cmake.sh | 0 contrib/ci/scripts/test_z3_install_cmake.sh | 0 contrib/ci/scripts/test_z3_system_tests.sh | 0 contrib/ci/scripts/test_z3_unit_tests_cmake.sh | 0 contrib/ci/scripts/travis_ci_entry_point.sh | 0 contrib/ci/scripts/travis_ci_linux_entry_point.sh | 0 contrib/ci/scripts/travis_ci_osx_entry_point.sh | 0 contrib/cmake/bootstrap.py | 0 scripts/build_libcxx_msan.sh | 0 scripts/mk_consts_files.py | 0 scripts/mk_def_file.py | 0 scripts/mk_gparams_register_modules_cpp.py | 0 scripts/mk_install_tactic_cpp.py | 0 scripts/mk_mem_initializer_cpp.py | 0 scripts/mk_pat_db.py | 0 scripts/pyg2hpp.py | 0 scripts/trackall.sh | 0 scripts/update_api.py | 0 src/math/lp/nla_core.cpp | 3 ++- 23 files changed, 2 insertions(+), 1 deletion(-) mode change 100755 => 100644 configure mode change 100755 => 100644 contrib/ci/scripts/build_z3_cmake.sh mode change 100755 => 100644 contrib/ci/scripts/install_deps_osx.sh mode change 100755 => 100644 contrib/ci/scripts/test_z3_docs.sh mode change 100755 => 100644 contrib/ci/scripts/test_z3_examples_cmake.sh mode change 100755 => 100644 contrib/ci/scripts/test_z3_install_cmake.sh mode change 100755 => 100644 contrib/ci/scripts/test_z3_system_tests.sh mode change 100755 => 100644 contrib/ci/scripts/test_z3_unit_tests_cmake.sh mode change 100755 => 100644 contrib/ci/scripts/travis_ci_entry_point.sh mode change 100755 => 100644 contrib/ci/scripts/travis_ci_linux_entry_point.sh mode change 100755 => 100644 contrib/ci/scripts/travis_ci_osx_entry_point.sh mode change 100755 => 100644 contrib/cmake/bootstrap.py mode change 100755 => 100644 scripts/build_libcxx_msan.sh mode change 100755 => 100644 scripts/mk_consts_files.py mode change 100755 => 100644 scripts/mk_def_file.py mode change 100755 => 100644 scripts/mk_gparams_register_modules_cpp.py mode change 100755 => 100644 scripts/mk_install_tactic_cpp.py mode change 100755 => 100644 scripts/mk_mem_initializer_cpp.py mode change 100755 => 100644 scripts/mk_pat_db.py mode change 100755 => 100644 scripts/pyg2hpp.py mode change 100755 => 100644 scripts/trackall.sh mode change 100755 => 100644 scripts/update_api.py diff --git a/configure b/configure old mode 100755 new mode 100644 diff --git a/contrib/ci/scripts/build_z3_cmake.sh b/contrib/ci/scripts/build_z3_cmake.sh old mode 100755 new mode 100644 diff --git a/contrib/ci/scripts/install_deps_osx.sh b/contrib/ci/scripts/install_deps_osx.sh old mode 100755 new mode 100644 diff --git a/contrib/ci/scripts/test_z3_docs.sh b/contrib/ci/scripts/test_z3_docs.sh old mode 100755 new mode 100644 diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh old mode 100755 new mode 100644 diff --git a/contrib/ci/scripts/test_z3_install_cmake.sh b/contrib/ci/scripts/test_z3_install_cmake.sh old mode 100755 new mode 100644 diff --git a/contrib/ci/scripts/test_z3_system_tests.sh b/contrib/ci/scripts/test_z3_system_tests.sh old mode 100755 new mode 100644 diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh old mode 100755 new mode 100644 diff --git a/contrib/ci/scripts/travis_ci_entry_point.sh b/contrib/ci/scripts/travis_ci_entry_point.sh old mode 100755 new mode 100644 diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh old mode 100755 new mode 100644 diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh old mode 100755 new mode 100644 diff --git a/contrib/cmake/bootstrap.py b/contrib/cmake/bootstrap.py old mode 100755 new mode 100644 diff --git a/scripts/build_libcxx_msan.sh b/scripts/build_libcxx_msan.sh old mode 100755 new mode 100644 diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py old mode 100755 new mode 100644 diff --git a/scripts/mk_def_file.py b/scripts/mk_def_file.py old mode 100755 new mode 100644 diff --git a/scripts/mk_gparams_register_modules_cpp.py b/scripts/mk_gparams_register_modules_cpp.py old mode 100755 new mode 100644 diff --git a/scripts/mk_install_tactic_cpp.py b/scripts/mk_install_tactic_cpp.py old mode 100755 new mode 100644 diff --git a/scripts/mk_mem_initializer_cpp.py b/scripts/mk_mem_initializer_cpp.py old mode 100755 new mode 100644 diff --git a/scripts/mk_pat_db.py b/scripts/mk_pat_db.py old mode 100755 new mode 100644 diff --git a/scripts/pyg2hpp.py b/scripts/pyg2hpp.py old mode 100755 new mode 100644 diff --git a/scripts/trackall.sh b/scripts/trackall.sh old mode 100755 new mode 100644 diff --git a/scripts/update_api.py b/scripts/update_api.py old mode 100755 new mode 100644 diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 78d1a657e..94371039b 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1474,9 +1474,10 @@ lbool core::check(vector& l_vec) { m_tangents.tangent_lemma(); } +#if 0 if (false && l_vec.empty() && !done()) ret = m_nra.check(); - +#endif if (ret == l_undef && !l_vec.empty() && m_reslim.inc()) ret = l_false;