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;