diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py
index d3f4027738b..58251c6f8d7 100644
--- a/scripts/mk_nuget_task.py
+++ b/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 @@ def create_nuget_spec(version, repo, branch, commit, symbols, arch):
© Microsoft Corporation. All rights reserved.
smt constraint solver theorem prover
content/icon.jpg
- content/README.md
https://github.com/Z3Prover/z3
MIT
@@ -119,10 +118,6 @@ def create_nuget_spec(version, repo, branch, commit, symbols, arch):
-
-
-
-
""".format(version, repo, branch, commit, arch)
print(contents)
sym = "sym." if symbols else ""
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 0728c2cb727..014b0e40f83 100644
--- a/scripts/mk_util.py
+++ b/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
diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml
index 2b1b4ca3d3c..0f533765409 100644
--- a/scripts/nightly.yaml
+++ b/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:
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index ee91b06a491..955025fd96c 100644
--- a/src/opt/opt_solver.cpp
+++ b/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) {
diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h
index b0d43bc00ac..edc640d86aa 100644
--- a/src/smt/theory_arith_pp.h
+++ b/src/smt/theory_arith_pp.h
@@ -83,9 +83,11 @@ namespace smt {
template
void theory_arith::display_row(std::ostream & out, row const & r, bool compact) const {
-
+ if (static_cast(r.get_base_var()) >= m_columns.size())
+ return;
column const & c = m_columns[r.get_base_var()];
- out << "(v" << r.get_base_var() << " r" << c[0].m_row_id << ") : ";
+ if (c.size() > 0)
+ out << "(v" << r.get_base_var() << " r" << c[0].m_row_id << ") : ";
bool first = true;
for (auto const& e : r) {
if (!e.is_dead()) {
diff --git a/src/util/tptr.h b/src/util/tptr.h
index 50e9417feea..37b6f64fe72 100644
--- a/src/util/tptr.h
+++ b/src/util/tptr.h
@@ -21,7 +21,6 @@ Revision History:
#include
#include "util/machine.h"
-#include
#define TAG_SHIFT PTR_ALIGNMENT
#define ALIGNMENT_VALUE (1 << PTR_ALIGNMENT)