Merge branch 'master' into polysat

src/CMakeLists.txt

@@ -207,7 +207,7 @@ if (MSVC)
       ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
       ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
     COMMENT "Generating \"${dll_module_exports_file}\""
-    ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+    USES_TERMINAL
     VERBATIM
   )
   add_custom_target(libz3_extra_depends

src/api/CMakeLists.txt

@@ -26,10 +26,8 @@ add_custom_command(OUTPUT ${generated_files}
   DEPENDS "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
           ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
           ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
-          # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
-          "${PROJECT_SOURCE_DIR}/scripts/mk_util.py"
   COMMENT "Generating ${generated_files}"
-  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+  USES_TERMINAL
   VERBATIM
 )
 

src/api/dotnet/CMakeLists.txt

@@ -19,7 +19,7 @@ add_custom_command(OUTPUT "${Z3_DOTNET_NATIVE_FILE}"
     "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
     ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
   COMMENT "Generating ${Z3_DOTNET_NATIVE_FILE}"
-  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+  USES_TERMINAL
 )
 
 # Generate Enumerations.cs
@@ -35,7 +35,7 @@ add_custom_command(OUTPUT "${Z3_DOTNET_CONST_FILE}"
     "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
     ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
   COMMENT "Generating ${Z3_DOTNET_CONST_FILE}"
-  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+  USES_TERMINAL
 )
 
 set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE

src/api/java/CMakeLists.txt

@@ -29,10 +29,8 @@ add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}"
     ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
     "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
     ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
-    # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
-    "${PROJECT_SOURCE_DIR}/scripts/mk_util.py"
   COMMENT "Generating \"${Z3_JAVA_NATIVE_JAVA}\" and \"${Z3_JAVA_NATIVE_CPP}\""
-  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+  USES_TERMINAL
 )
 
 # Add rule to build native code that provides a bridge between
@@ -88,7 +86,7 @@ add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
     "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
     ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
   COMMENT "Generating ${Z3_JAVA_PACKAGE_NAME}.enumerations package"
-  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+  USES_TERMINAL
 )
 
 set(Z3_JAVA_JAR_SOURCE_FILES

src/api/python/CMakeLists.txt

@@ -43,7 +43,7 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py"
     "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
     ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
   COMMENT "Generating z3core.py"
-  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+  USES_TERMINAL
 )
 list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3core.py")
 
@@ -59,7 +59,7 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3consts.py"
     "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
     ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
   COMMENT "Generating z3consts.py"
-  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+  USES_TERMINAL
 )
 list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3consts.py")
 

src/ast/pattern/CMakeLists.txt

@@ -15,7 +15,7 @@ add_custom_command(OUTPUT "database.h"
   DEPENDS "${PROJECT_SOURCE_DIR}/scripts/mk_pat_db.py"
           ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
   COMMENT "Generating \"database.h\""
-  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+  USES_TERMINAL
   VERBATIM
 )
 

src/ast/pattern/pattern_inference.cpp

@@ -106,7 +106,7 @@ pattern_inference_cfg::pattern_inference_cfg(ast_manager & m, pattern_inference_
     m_params(params),
     m_bfid(m.get_basic_family_id()),
     m_afid(m.mk_family_id("arith")),
-    m_le(m),
+    m_le(),
     m_nested_arith_only(true),
     m_block_loop_patterns(params.m_pi_block_loop_patterns),
     m_candidates(m),

src/ast/pattern/pattern_inference.h

@@ -37,7 +37,6 @@ Revision History:
    every instance of f(g(X)) is also an instance of f(X).
 */
 class smaller_pattern {
-    ast_manager &    m;
     ptr_vector<expr> m_bindings;
 
     typedef std::pair<expr *, expr *> expr_pair;
@@ -50,9 +49,7 @@ class smaller_pattern {
 
 public:
 
-    smaller_pattern(ast_manager & m):
-        m(m) {
-    }
+    smaller_pattern() = default;
 
     smaller_pattern & operator=(smaller_pattern const &) = delete;
 

src/smt/theory_array.cpp

@@ -91,9 +91,9 @@ namespace smt {
         d->m_parent_selects.push_back(s);
         TRACE("array", tout << v << " " << mk_pp(s->get_expr(), m) << " " << mk_pp(get_enode(v)->get_expr(), m) << "\n";);
         m_trail_stack.push(push_back_trail<enode *, false>(d->m_parent_selects));
-        for (enode* n : d->m_stores) {
+        for (enode* n : d->m_stores) 
             instantiate_axiom2a(s, n);
-        }
+
         if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
             for (enode* store : d->m_parent_stores) {
                 SASSERT(is_store(store));

src/smt/theory_array_base.cpp

@@ -179,6 +179,12 @@ namespace smt {
                 conseq_expr = ctx.bool_var2expr(conseq.var());
             }
 
+            if (m.are_distinct(idx1->get_expr(), idx2->get_expr())) {
+                ctx.mark_as_relevant(conseq);
+                assert_axiom(conseq);
+                continue;
+            }
+
             literal ante = mk_eq(idx1->get_expr(), idx2->get_expr(), true);
             ctx.mark_as_relevant(ante);
             // ctx.force_phase(ante);

src/test/lp/lp.cpp

@@ -19,7 +19,7 @@
   --*/
 
 #include <limits>
-#if _LINUX_
+#ifndef _WINDOWS
 #include <dirent.h>
 #endif
 #include <algorithm>
@@ -1735,7 +1735,7 @@ void random_test() {
     }
 }
 
-#if _LINUX_
+#ifndef _WINDOWS
 void fill_file_names(vector<std::string> &file_names,  std::set<std::string> & minimums) {
     char *home_dir = getenv("HOME");
     if (home_dir == nullptr) {
@@ -1885,7 +1885,7 @@ void test_out_dir(std::string out_dir) {
 
 void find_dir_and_file_name(std::string a, std::string & dir, std::string& fn) {
     // todo: make it system independent
-    size_t last_slash_pos = a.find_last_of("/");
+    size_t last_slash_pos = a.find_last_of('/');
     if (last_slash_pos >= a.size()) {
         std::cout << "cannot find file name in " << a << std::endl;
         throw;
@@ -4072,7 +4072,7 @@ void test_lp_local(int argn, char**argv) {
     }
     
     if (args_parser.option_is_used("--solve_some_mps")) {
-#if _LINUX_
+#ifndef _WINDOWS
         solve_some_mps(args_parser);
 #endif
         ret = 0;

src/util/env_params.cpp

@@ -28,7 +28,7 @@ void env_params::updt_params() {
     enable_warning_messages(p.get_bool("warning", true));
     memory::set_max_size(megabytes_to_bytes(p.get_uint("memory_max_size", 0)));
     memory::set_max_alloc_count(p.get_uint("memory_max_alloc_count", 0));
-    memory::set_high_watermark(p.get_uint("memory_high_watermark", 0));
+    memory::set_high_watermark(megabytes_to_bytes(p.get_uint("memory_high_watermark", 0)));
 }
 
 void env_params::collect_param_descrs(param_descrs & d) {