Merge branch 'master' of https://github.com/z3prover/z3

scripts/mk_nuget_task.py

@@ -88,7 +88,7 @@ def mk_targets(source_root):
 def mk_icon(source_root):
     mk_dir("out/content")
     shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg")
-    shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md")
+#   shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md")
 
 
     
@@ -109,7 +109,6 @@ Linux Dependencies:
         <copyright>&#169; Microsoft Corporation. All rights reserved.</copyright>
         <tags>smt constraint solver theorem prover</tags>
         <icon>content/icon.jpg</icon>
-        <readme>content/README.md</readme>
         <projectUrl>https://github.com/Z3Prover/z3</projectUrl>
         <license type="expression">MIT</license>
         <repository type="git" url="{1}" branch="{2}" commit="{3}" />
@@ -119,10 +118,6 @@ Linux Dependencies:
             <group targetFramework=".netstandard2.0" />
         </dependencies>
     </metadata>
-    <files>
-      <file src="content/README.md" target="content/README.md"/>
-      <file src="content/icon.jpg" target="content/icon.jpg"/>
-    </files>
 </package>""".format(version, repo, branch, commit, arch)
     print(contents)
     sym = "sym." if symbols else ""

scripts/mk_util.py

@@ -2994,9 +2994,19 @@ def cp_z3py_to_build():
         for f in files:
             if f.endswith('.pyc'):
                 rmf(os.path.join(root, f))
+    # We do not want a second copy of the compiled files in the system-wide cache,
+    # so we disable it temporarily. This is an issue with recent versions of MacOS
+    # where XCode's Python has a cache, but the build scripts don't have access to
+    # it (e.g. during OPAM package installation).
+    have_cache = hasattr(sys, 'pycache_prefix') and sys.pycache_prefix is not None
+    if have_cache:
+        pycache_prefix_before = sys.pycache_prefix
+        sys.pycache_prefix = None
     # Compile Z3Py files
     if compileall.compile_dir(z3py_src, force=1) != 1:
         raise MKException("failed to compile Z3Py sources")
+    if have_cache:
+        sys.pycache_prefix = pycache_prefix_before
     if is_verbose:
         print("Generated python bytecode")
     # Copy sources to build

scripts/nightly.yaml

@@ -233,6 +233,48 @@ stages:
         symbolServerType: TeamServices
         detailedLog: true
 
+  - job: "WindowsArm64"
+    displayName: "WindowsArm64"
+    pool: 
+      vmImage: "windows-latest"
+    variables:
+       arch: "amd64_arm64"
+       bindings: "-DCMAKE_BUILD_TYPE=RelWithDebInfo"
+    steps:
+    - script: md build
+    - script: |
+         cd build
+         call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" $(arch)
+         cmake $(bindings) -G "NMake Makefiles" ../
+         nmake
+         cd ..
+    - task: CopyFiles@2
+      inputs:
+        sourceFolder: build
+        contents: '*z3*.*'
+        targetFolder: $(Build.ArtifactStagingDirectory)
+    - task: PublishPipelineArtifact@1
+      inputs:
+        targetPath: $(Build.ArtifactStagingDirectory)
+        artifactName: 'WindowsArm64'
+    - task: CopyFiles@2
+      displayName: 'Collect Symbols'
+      inputs:
+        sourceFolder: build
+        contents: '**/*.pdb'
+        targetFolder: '$(Build.ArtifactStagingDirectory)/symbols'
+    # Publish symbol archive to match nuget package
+    # Index your source code and publish symbols to a file share or Azure Artifacts symbol server
+    - task: PublishSymbols@2
+      inputs:
+        symbolsFolder: '$(Build.ArtifactStagingDirectory)/symbols'
+        searchPattern: '**/*.pdb' 
+        indexSources: false # Github not supported
+        publishSymbols: true
+        symbolServerType: TeamServices
+        detailedLog: true
+
+
 - stage: Package
   jobs:
   - job: NuGet64
@@ -534,6 +576,11 @@ stages:
       inputs:
         artifactName: 'Windows32'
         targetPath: tmp
+    - task: DownloadPipelineArtifact@2
+      displayName: "Download windowsArm64"
+      inputs:
+        artifactName: 'WindowsArm64'
+        targetPath: tmp
     - task: DownloadPipelineArtifact@2
       displayName: "Download windows64"
       inputs:

src/opt/opt_solver.cpp

@@ -52,7 +52,7 @@ namespace opt {
         if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {            
             m_params.m_relevancy_lvl = 0;
         }
-        m_params.m_arith_auto_config_simplex = false;
+        m_params.m_arith_auto_config_simplex = true;
         m_params.m_threads = 1; // need to interact with the solver that created model so can't have threads
         // m_params.m_auto_config = false;
     }
@@ -67,7 +67,7 @@ namespace opt {
         m_dump_benchmarks = p.dump_benchmarks();
         m_params.updt_params(_p);
         m_context.updt_params(_p);
-        m_params.m_arith_auto_config_simplex = false;
+        m_params.m_arith_auto_config_simplex = true;
     }
 
     solver* opt_solver::translate(ast_manager& m, params_ref const& p) {

src/smt/theory_arith_pp.h

@@ -83,8 +83,10 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::display_row(std::ostream & out, row const & r, bool compact) const {
-
+        if (static_cast<unsigned>(r.get_base_var()) >= m_columns.size())
+            return;
         column const & c   = m_columns[r.get_base_var()];
+        if (c.size() > 0)
             out << "(v" << r.get_base_var() << " r" << c[0].m_row_id << ") : ";
         bool first = true;
         for (auto const& e : r) {

src/util/tptr.h

@@ -21,7 +21,6 @@ Revision History:
 
 #include <cstdint>
 #include "util/machine.h"
-#include <cstdint>
 
 #define TAG_SHIFT        PTR_ALIGNMENT
 #define ALIGNMENT_VALUE  (1 << PTR_ALIGNMENT)