From c174df4071783ca81c03e38bf8ceccc18f196c05 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Mon, 8 Jun 2026 11:21:54 -0700 Subject: [PATCH 01/14] Allow FStar build failures without blocking build-and-report workflow progression (#9769) `build-and-report` was failing hard when the `Build FStar` step hit prover regressions, preventing downstream reporting from running. This change makes FStar failures non-blocking and ensures the reporting path still executes with an explicit FStar outcome. - **Workflow failure propagation** - Marked `Build FStar` as non-blocking: - added `id: build_fstar` - added `continue-on-error: true` - **Guaranteed reporting execution** - Made the summary step unconditional with `if: always()` so it runs even when FStar fails. - **Robust summary generation** - Passed step outcome into the script (`FSTAR_BUILD_OUTCOME`). - Hardened file reads for missing FStar artifacts/version files. - Report body now reflects actual FStar outcome (`success` vs non-success) while preserving pipeline continuity. ```yaml - name: Build FStar id: build_fstar continue-on-error: true run: | # existing FStar build commands - name: Create discussion summary if: always() env: FSTAR_BUILD_OUTCOME: ${{ steps.build_fstar.outcome }} uses: actions/github-script@v9 ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- .github/workflows/fstar-master-build.yml | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml index 4b674fc33..f5b9417f2 100644 --- a/.github/workflows/fstar-master-build.yml +++ b/.github/workflows/fstar-master-build.yml @@ -86,6 +86,8 @@ jobs: /tmp/gh-aw/agent/z3-bin/z3 --version - name: Build FStar + id: build_fstar + continue-on-error: true run: | set -euo pipefail rm -rf /tmp/gh-aw/agent/FStar @@ -106,18 +108,26 @@ jobs: /tmp/gh-aw/agent/FStar/out/bin/fstar.exe --version | tee /tmp/gh-aw/agent/fstar-version.txt - name: Create discussion summary + if: always() uses: actions/github-script@v9 env: RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }} + FSTAR_BUILD_OUTCOME: ${{ steps.build_fstar.outcome }} with: script: | const fs = require('fs'); - const z3VersionText = fs.readFileSync('/tmp/gh-aw/agent/z3-version.txt', 'utf8').trim(); - const fstarVersionFile = fs.readFileSync('/tmp/gh-aw/agent/fstar-version.txt', 'utf8').trim(); + const readIfExists = (path) => fs.existsSync(path) ? fs.readFileSync(path, 'utf8').trim() : null; + const z3VersionText = readIfExists('/tmp/gh-aw/agent/z3-version.txt') ?? 'unknown'; + const fstarVersionFile = readIfExists('/tmp/gh-aw/agent/fstar-version.txt') ?? ''; const fstarVersionText = fstarVersionFile ? fstarVersionFile.split('\n')[0] : 'unknown'; - const fstarCommitLine = fs.readFileSync('/tmp/gh-aw/agent/fstar-commit.txt', 'utf8').trim(); - const fstarCommit = fstarCommitLine.replace(/^FStar commit:\s*/, ''); + const fstarCommitLine = readIfExists('/tmp/gh-aw/agent/fstar-commit.txt') ?? ''; + const fstarCommit = fstarCommitLine ? fstarCommitLine.replace(/^FStar commit:\s*/, '') : 'unknown'; + const fstarBuildOutcome = process.env.FSTAR_BUILD_OUTCOME || 'unknown'; + const fstarBuildSucceeded = fstarBuildOutcome === 'success'; + const fstarStatus = fstarBuildSucceeded + ? '✅ FStar build completed' + : `⚠️ FStar build ${fstarBuildOutcome} (pipeline continued)`; const date = new Date().toISOString().slice(0, 10); const owner = context.repo.owner; @@ -146,7 +156,7 @@ jobs: const body = [ `### Build status`, `- ✅ Z3 build completed`, - `- ✅ FStar build completed`, + `- ${fstarStatus}`, ``, `### Inputs used`, `- z3_ref: \`${process.env.Z3_REF}\``, From 0cc04b53eba4bd54e4f4f013c4dd8f988b09a67f Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Mon, 8 Jun 2026 15:40:38 -0700 Subject: [PATCH 02/14] [code-simplifier] Consolidate repo-root helpers and simplify skill script logic (#9772) This change simplifies recently touched skill scripts by removing duplicated repo-root discovery code, promoting shared root lookup to a public API, and tightening small readability issues without changing behavior. It keeps script semantics intact while making cross-skill reuse explicit. - **Shared API cleanup (`.github/skills/shared/z3db.py`)** - Promote `_find_repo_root` to public `find_repo_root`. - Add `require_repo_root()` for scripts that should fail-fast when root discovery fails. - Update library usage docstring to expose both helpers. - Replace adjacent SQL string literals in `log()` with a single literal. - **Deduplicate memory-safety root lookup (`.github/skills/memory-safety/scripts/memory_safety.py`)** - Remove local `find_repo_root()` implementation. - Import and use shared `require_repo_root()` from `z3db`. - **Simplify static-analysis label selection (`.github/skills/static-analysis/scripts/static_analysis.py`)** - Replace two-step label assignment with a single expression: - `label = f["type"] or f["category"]` ```python # before label = f["category"] if f["type"]: label = f["type"] # after label = f["type"] or f["category"] ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- .../memory-safety/scripts/memory_safety.py | 17 ++--------------- .github/skills/shared/z3db.py | 18 ++++++++++++++---- .../static-analysis/scripts/static_analysis.py | 4 +--- 3 files changed, 17 insertions(+), 22 deletions(-) diff --git a/.github/skills/memory-safety/scripts/memory_safety.py b/.github/skills/memory-safety/scripts/memory_safety.py index fa87f8f8c..10fb8ec82 100644 --- a/.github/skills/memory-safety/scripts/memory_safety.py +++ b/.github/skills/memory-safety/scripts/memory_safety.py @@ -18,7 +18,7 @@ import time from pathlib import Path sys.path.insert(0, str(Path(__file__).resolve().parent.parent.parent / "shared")) -from z3db import Z3DB, setup_logging +from z3db import Z3DB, require_repo_root, setup_logging logger = logging.getLogger("z3agent") @@ -52,19 +52,6 @@ def check_dependencies(): sys.exit(1) -def find_repo_root() -> Path: - d = Path.cwd() - for _ in range(10): - if (d / "CMakeLists.txt").exists() and (d / "src").is_dir(): - return d - parent = d.parent - if parent == d: - break - d = parent - logger.error("could not locate Z3 repository root") - sys.exit(1) - - def build_is_configured(build_dir: Path, sanitizer: str) -> bool: """Check whether the build directory already has a matching cmake config.""" cache = build_dir / "CMakeCache.txt" @@ -220,7 +207,7 @@ def main(): setup_logging(args.debug) check_dependencies() - repo_root = find_repo_root() + repo_root = require_repo_root() sanitizers = ["asan", "ubsan"] if args.sanitizer == "both" else [args.sanitizer] all_findings = [] diff --git a/.github/skills/shared/z3db.py b/.github/skills/shared/z3db.py index f0f7e3ea2..0d49cb7cf 100644 --- a/.github/skills/shared/z3db.py +++ b/.github/skills/shared/z3db.py @@ -3,7 +3,7 @@ z3db: shared library and CLI for Z3 skill scripts. Library usage: - from z3db import Z3DB, find_z3, run_z3 + from z3db import Z3DB, find_z3, find_repo_root, require_repo_root, run_z3 CLI usage: python z3db.py init @@ -131,7 +131,7 @@ class Z3DB: """Write to stderr and to the interaction_log table.""" getattr(logger, level, logger.info)(message) self.conn.execute( - "INSERT INTO interaction_log (run_id, level, message) " "VALUES (?, ?, ?)", + "INSERT INTO interaction_log (run_id, level, message) VALUES (?, ?, ?)", (run_id, level, message), ) self.conn.commit() @@ -182,7 +182,7 @@ def find_z3(hint: str = None) -> str: if hint: candidates.append(hint) - repo_root = _find_repo_root() + repo_root = find_repo_root() if repo_root: for build_dir in ["build", "build/release", "build/debug"]: candidates.append(str(repo_root / build_dir / "z3")) @@ -201,7 +201,8 @@ def find_z3(hint: str = None) -> str: sys.exit(1) -def _find_repo_root() -> Optional[Path]: +def find_repo_root() -> Optional[Path]: + """Best-effort search for the Z3 repository root from the current directory.""" d = Path.cwd() for _ in range(10): if (d / "CMakeLists.txt").exists() and (d / "src").is_dir(): @@ -213,6 +214,15 @@ def _find_repo_root() -> Optional[Path]: return None +def require_repo_root() -> Path: + """Return the Z3 repository root or exit the process if it is not found.""" + repo_root = find_repo_root() + if repo_root is None: + logger.error("could not locate Z3 repository root") + sys.exit(1) + return repo_root + + def run_z3( formula: str, z3_bin: str = None, diff --git a/.github/skills/static-analysis/scripts/static_analysis.py b/.github/skills/static-analysis/scripts/static_analysis.py index 65f87e731..f93e43692 100644 --- a/.github/skills/static-analysis/scripts/static_analysis.py +++ b/.github/skills/static-analysis/scripts/static_analysis.py @@ -176,9 +176,7 @@ def print_findings(findings: list): return for f in findings: - label = f["category"] - if f["type"]: - label = f["type"] + label = f["type"] or f["category"] print(f"[{label}] {f['file']}:{f['line']}: {f['description']}") print() From 2ed4e90c758608cf8744da8f1d2fca945154373c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Mon, 8 Jun 2026 19:35:04 -0700 Subject: [PATCH 03/14] Fix Java UnsatisfiedLinkError on macOS (#7640) (#9027) On macOS, libz3java.dylib was built without an rpath to find libz3.dylib in the same directory. When Java loaded the JNI library, the dynamic linker could not resolve the libz3 dependency, causing UnsatisfiedLinkError. Three fixes: - mk_util.py: add -Wl,-rpath,@loader_path to the macOS JNI link command - CMakeLists.txt: set MACOSX_RPATH, BUILD_RPATH, INSTALL_RPATH for z3java target; remove duplicate headerpad block - update_api.py: improve Native.java error message to show the root cause from both load attempts instead of only the fallback error Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- scripts/mk_util.py | 3 +++ scripts/tests/test_jni_arch_flags.py | 39 ++++++++++++++++++++++++++++ scripts/update_api.py | 11 +++++++- src/api/java/CMakeLists.txt | 13 +++++----- 4 files changed, 59 insertions(+), 7 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 8b862fec2..ff04bfb68 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1919,6 +1919,9 @@ class JavaDLLComponent(Component): if IS_WINDOWS: # On Windows, CL creates a .lib file to link against. out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' % os.path.join('api', 'java', 'Native')) + elif IS_OSX: + out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT) -Wl,-rpath,@loader_path $(SLINK_EXTRA_FLAGS)\n' % + os.path.join('api', 'java', 'Native')) else: out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT) $(SLINK_EXTRA_FLAGS)\n' % os.path.join('api', 'java', 'Native')) diff --git a/scripts/tests/test_jni_arch_flags.py b/scripts/tests/test_jni_arch_flags.py index 2796b156d..e60285eec 100644 --- a/scripts/tests/test_jni_arch_flags.py +++ b/scripts/tests/test_jni_arch_flags.py @@ -208,6 +208,45 @@ class TestJNIArchitectureFlagsInMakefile(unittest.TestCase): "(the import library)", ) + # ------------------------------------------------------------------ + # Tests for macOS rpath, so libz3java.dylib can find libz3.dylib + # ------------------------------------------------------------------ + + def test_macos_uses_loader_path_rpath(self): + """ + On macOS, the JNI link command must include -Wl,-rpath,@loader_path + so that libz3java.dylib can find libz3.dylib in the same directory + at runtime. Without this, Java fails with UnsatisfiedLinkError. + """ + comp = self._make_java_dll_component() + text = self._generate_makefile( + comp, is_windows=False, is_osx=True, is_arch_arm64=True + ) + link_lines = self._find_jni_link_lines(text) + self.assertTrue(link_lines, "Expected at least one JNI link line") + for line in link_lines: + self.assertIn( + '-Wl,-rpath,@loader_path', line, + "macOS JNI link command must set rpath to @loader_path " + "so libz3java.dylib finds libz3.dylib at runtime", + ) + + def test_linux_does_not_use_loader_path(self): + """ + On Linux, @loader_path is a macOS concept and must not appear. + """ + comp = self._make_java_dll_component() + text = self._generate_makefile( + comp, is_windows=False, is_osx=False, is_arch_arm64=False + ) + link_lines = self._find_jni_link_lines(text) + self.assertTrue(link_lines, "Expected at least one JNI link line") + for line in link_lines: + self.assertNotIn( + '@loader_path', line, + "@loader_path is macOS-specific and must not appear on Linux", + ) + # ------------------------------------------------------------------ # Consistency check: SLINK_EXTRA_FLAGS in mk_config for cross-compile # ------------------------------------------------------------------ diff --git a/scripts/update_api.py b/scripts/update_api.py index df80da116..b539165a3 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -631,7 +631,16 @@ def mk_java(java_src, java_dir, package_name): java_native.write(' try {\n') java_native.write(' System.loadLibrary("z3java");\n') java_native.write(' } catch (UnsatisfiedLinkError ex) {\n') - java_native.write(' System.loadLibrary("libz3java");\n') + java_native.write(' try {\n') + java_native.write(' System.loadLibrary("libz3java");\n') + java_native.write(' } catch (UnsatisfiedLinkError ex2) {\n') + java_native.write(' throw new UnsatisfiedLinkError(\n') + java_native.write(' "Failed to load z3java native library. "\n') + java_native.write(' + "Tried z3java: " + ex.getMessage() + "; "\n') + java_native.write(' + "Tried libz3java: " + ex2.getMessage() + ". "\n') + java_native.write(' + "Make sure both the JNI library and libz3 are in java.library.path "\n') + java_native.write(' + "or set DYLD_LIBRARY_PATH (macOS) / LD_LIBRARY_PATH (Linux).");\n') + java_native.write(' }\n') java_native.write(' }\n') java_native.write(' }\n') java_native.write(' }\n') diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 194b25232..774a293bc 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -48,17 +48,18 @@ target_include_directories(z3java PRIVATE "${PROJECT_BINARY_DIR}/src/api" ${JNI_INCLUDE_DIRS} ) -# Add header padding for macOS to allow install_name_tool to modify the dylib +# On macOS, set rpath so libz3java.dylib can find libz3.dylib in the same directory, +# and add header padding to allow install_name_tool to modify the dylib. if (CMAKE_SYSTEM_NAME STREQUAL "Darwin") + set_target_properties(z3java PROPERTIES + MACOSX_RPATH TRUE + INSTALL_RPATH "@loader_path" + BUILD_RPATH "@loader_path" + ) target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names") endif() # FIXME: Should this library have SONAME and VERSION set? -# On macOS, add headerpad for install_name_tool compatibility -if(CMAKE_SYSTEM_NAME STREQUAL "Darwin") - target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names") -endif() - # This prevents CMake from automatically defining ``z3java_EXPORTS`` set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "") From aa872bd289ae9a2d7dfe6a2da079baa0400f24a8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Mon, 8 Jun 2026 19:35:49 -0700 Subject: [PATCH 04/14] spacer: enable model completion in arith qe_project (#9776) Variables to be projected may not be assigned in the model (e.g. grounded auxiliary variables that are don't-cares). Enable model completion in the arith `qe_project` so their evaluation yields concrete numerals, matching the behavior of the native MBP arith projector. Two call sites in `arith_project_util` (`src/muz/spacer/spacer_qe_project.cpp`) now install a `model::scoped_model_completion` before evaluating projected variables against the model. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/muz/spacer/spacer_qe_project.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index d47a09d14..58499c028 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -1148,6 +1148,7 @@ class arith_project_util { expr_ref_vector const &lits) { app_ref_vector new_vars(m); expr_ref_vector result(lits); + model::scoped_model_completion _smc(mdl, true); for (unsigned i = 0; i < vars.size(); ++i) { app *v = vars.get(i); m_var = alloc(contains_app, m, v); @@ -1183,6 +1184,12 @@ class arith_project_util { expr_map &map) { app_ref_vector new_vars(m); + // Variables to be projected may not be assigned in the model + // (e.g. grounded auxiliary variables that are don't-cares). Enable + // model completion so their evaluation yields concrete numerals, + // matching the behavior of the native MBP arith projector. + model::scoped_model_completion _smc(mdl, true); + // factor out mod terms by introducing new variables TRACE(qe, tout << "before factoring out mod terms:" << "\n"; tout << mk_pp(fml, m) << "\n"; tout << "mdl:\n"; From 49014fe30231728e4ea05847e1fefe8da2a8e0ae Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Mon, 8 Jun 2026 19:36:14 -0700 Subject: [PATCH 05/14] Fix right-side `can_add` indexing in `sls_seq_plugin` edit-distance repair (#9773) `seq_plugin::edit_distance_with_updates` used the left-string DP index when checking whether the right string could accept an insertion from the `d[i][j - 1]` transition. This miscomputed updateable edit distance and could suppress valid repair proposals when `i != j`. - **Bug fix** - Change the right-side insertion guard in `src/ast/sls/sls_seq_plugin.cpp` from `b.can_add(i - 1)` to `b.can_add(j - 1)`. - This aligns the mutability check with the DP transition being evaluated and with the existing update-generation logic below it. - **Regression coverage** - Add a focused test in `src/test/sls_seq_plugin.cpp` for an asymmetric variable/value layout on the right-hand side. - The test asserts that the repair logic admits the right-side add at `j - 1`, which is the case that the previous index mixup could reject. - **Reference** - The updated condition now matches the intended transition semantics: ```cpp if (d[i][j - 1] < u[i][j] && b.can_add(j - 1)) { m_string_updates.reset(); u[i][j] = d[i][j - 1]; } ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/ast/sls/sls_seq_plugin.cpp | 2 +- src/test/sls_seq_plugin.cpp | 24 ++++++++++++++++++++++++ 2 files changed, 25 insertions(+), 1 deletion(-) diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index f516b2948..8584741f3 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -912,7 +912,7 @@ namespace sls { m_string_updates.reset(); u[i][j] = d[i - 1][j]; } - if (d[i][j - 1] < u[i][j] && b.can_add(i - 1)) { + if (d[i][j - 1] < u[i][j] && b.can_add(j - 1)) { m_string_updates.reset(); u[i][j] = d[i][j - 1]; } diff --git a/src/test/sls_seq_plugin.cpp b/src/test/sls_seq_plugin.cpp index b7a23a596..4c8c5340c 100644 --- a/src/test/sls_seq_plugin.cpp +++ b/src/test/sls_seq_plugin.cpp @@ -351,4 +351,28 @@ void tst_sls_seq_plugin() { app_ref eq(m.mk_eq(l, r), m); verbose_stream() << eq << "\n"; ts.repair_down_str_eq_edit_distance_incremental(eq); + + test_seq::string_instance lhs, rhs; + lhs.s = zstring("a"); + lhs.is_value.push_back(false); + lhs.prev_is_var.push_back(false); + lhs.next_is_var.push_back(false); + rhs.s = zstring("ab"); + rhs.is_value.push_back(true); + rhs.prev_is_var.push_back(false); + rhs.next_is_var.push_back(false); + rhs.is_value.push_back(false); + rhs.prev_is_var.push_back(false); + rhs.next_is_var.push_back(false); + + ENSURE(ts.edit_distance_with_updates(lhs, rhs) == 0); + ENSURE(ts.m_string_updates.size() == 2); + ENSURE(ts.m_string_updates[0].side == test_seq::side_t::right); + ENSURE(ts.m_string_updates[0].op == test_seq::op_t::add); + ENSURE(ts.m_string_updates[0].i == 0); + ENSURE(ts.m_string_updates[0].j == 1); + ENSURE(ts.m_string_updates[1].side == test_seq::side_t::right); + ENSURE(ts.m_string_updates[1].op == test_seq::op_t::del); + ENSURE(ts.m_string_updates[1].i == 1); + ENSURE(ts.m_string_updates[1].j == 0); } \ No newline at end of file From 69cd7e0c4c6437c53bf8fe4e380a77ab57e0a6bb Mon Sep 17 00:00:00 2001 From: davedets Date: Mon, 8 Jun 2026 19:44:01 -0700 Subject: [PATCH 06/14] Fixes necessary to compile z3 included in clang-tidy via FetchContents. (#9768) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The page https://github.com/Z3Prover/z3/blob/master/README-CMake.md#adding-z3-as-a-dependency-to-a-cmake-project advises using the CMake FetchContent feature to include z3 as source into other CMake project. I'm trying to do this to use Z3 within a ClangTidy checker. This is one of a series of PR's aimed at getting Z3 to compile cleanly when included this way. This initial PR fixes all the errors, allowing the compilation to succeed. Subsequent diffs will address warnings. I tested only the CMake compilation, on a Mac. *Missing Z3_THROWs* Update z3++.h to use Z3_THROW in a couple of places. Clang compiles with exceptions disabled so we get messages like: ``` /Users/daviddetlefs/llvm-project/build_dbg/_deps/z3-src/src/api/c++/z3++.h:4928:17: error: cannot use 'throw' with exceptions disabled4928 | throw exception("rcf_num objects from different contexts"); ``` NOTE TO REVIEWERS: I'm not complete clear on the usage conventions for Z3_THROW. With exception disabled, it seems like the throwing function will just continue. If there's somethign else that should be done, like setting some error state, please let me know. *CMake component name collision* There was an error at the CMake level, a name collision (on "opt"). Apparently CMake components are named using a flat namespace, so it's easy to see how this could occur. It seems to me that the right global way to fix this would be to encourage people to use some form of "qualified name" convention in naming their component. The fix I chose was a local version of this, changing the Z3 component name to z3_opt. (It didn't seem feasible to make the change in clang.) NOTE TO REVIEWERS: If you think this is OK, please let me know if a) You'd like me to also change the name of the opt directory, to keep thecomponent-name == directory-name invariant, and b) You'd like me to make this z3_ change more globally, to future-proof (somewhat) against similar component name collisions. --- src/api/CMakeLists.txt | 2 +- src/api/c++/z3++.h | 6 +++--- src/opt/CMakeLists.txt | 2 +- src/shell/CMakeLists.txt | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index c1e78f473..c6ad57c70 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -66,7 +66,7 @@ z3_add_component(api z3_replayer.cpp ${full_path_generated_files} COMPONENT_DEPENDENCIES - opt + z3_opt euf portfolio realclosure diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index f66bd1f76..9e8cc6796 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -4925,7 +4925,7 @@ namespace z3 { void check_context(rcf_num const& other) const { if (m_ctx != other.m_ctx) { - throw exception("rcf_num objects from different contexts"); + Z3_THROW(exception("rcf_num objects from different contexts")); } } @@ -5105,9 +5105,9 @@ namespace z3 { */ inline std::vector rcf_roots(context& c, std::vector const& coeffs) { if (coeffs.empty()) { - throw exception("polynomial coefficients cannot be empty"); + Z3_THROW(exception("polynomial coefficients cannot be empty")); } - + unsigned n = static_cast(coeffs.size()); std::vector a(n); std::vector roots(n); diff --git a/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt index 21075d88c..85b716306 100644 --- a/src/opt/CMakeLists.txt +++ b/src/opt/CMakeLists.txt @@ -1,4 +1,4 @@ -z3_add_component(opt +z3_add_component(z3_opt SOURCES maxcore.cpp maxlex.cpp diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index c0e9c8505..22c071966 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -8,7 +8,7 @@ set (shell_object_files "") # We are only using these dependencies to enforce a build # order. We don't use this list for actual linking. -set(shell_deps api extra_cmds opt sat) +set(shell_deps api extra_cmds z3_opt sat) z3_expand_dependencies(shell_expanded_deps ${shell_deps}) get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS) foreach (component ${Z3_LIBZ3_COMPONENTS_LIST}) From 3d6e223f9eb8d6d7f199ae7bcbd6dc361265a9f9 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Mon, 8 Jun 2026 23:15:42 -0700 Subject: [PATCH 07/14] Route memory-safety ASan/UBSan reporting to GitHub issues instead of discussions (#9785) The memory-safety scan workflow already runs ASan/UBSan, but its reporting workflow was configured to post discussions rather than filing actionable issues. This change aligns the reporter with the expected outcome: sanitizer findings become trackable GitHub issues. - **Reporting output switched to issues** - Replaced `safe-outputs.create-discussion` with `safe-outputs.create-issue` in `memory-safety-report.md` - Added issue labels and issue cap for controlled issue creation - Updated workflow description text to reflect issue-based reporting - **Prompt behavior updated for clean/noisy runs** - Updated agent instructions to generate issue reports for actionable findings - Changed zero-finding behavior to `noop` (no issue spam on clean runs) - Updated wording for failure/edge-case paths to reference issue output - **Compiled workflow updated** - Regenerated `memory-safety-report.lock.yml` from the markdown source so runtime behavior matches the new safe-output contract ```yaml safe-outputs: create-issue: title-prefix: "[Memory Safety] " labels: [bug, memory-safety, automated-analysis] max: 1 noop: report-as-issue: false ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- .../workflows/memory-safety-report.lock.yml | 68 ++++++++++--------- .github/workflows/memory-safety-report.md | 20 +++--- 2 files changed, 46 insertions(+), 42 deletions(-) diff --git a/.github/workflows/memory-safety-report.lock.yml b/.github/workflows/memory-safety-report.lock.yml index 647fce0b3..f563a1476 100644 --- a/.github/workflows/memory-safety-report.lock.yml +++ b/.github/workflows/memory-safety-report.lock.yml @@ -1,4 +1,4 @@ -# gh-aw-metadata: {"schema_version":"v4","frontmatter_hash":"3ed9f3a1cb53ff5095a4ff6a8169b75a50977baeddb965694ad30555729d56e4","body_hash":"3fece373efec3e8c9950482fd433a5bb06b3eb702a2e638af34815f937642fbe","compiler_version":"v0.77.5","strict":true,"agent_id":"copilot"} +# gh-aw-metadata: {"schema_version":"v4","frontmatter_hash":"01e10498ee43530594fb5994a345b01b5718ffabe2872be157994f5489d81dad","body_hash":"f43683a4995003e2678ccce2706b639eb627b48daeafc7f9dded40d4508ef26c","compiler_version":"v0.77.5","strict":true,"agent_id":"copilot"} # gh-aw-manifest: {"version":1,"secrets":["COPILOT_GITHUB_TOKEN","GH_AW_GITHUB_MCP_SERVER_TOKEN","GH_AW_GITHUB_TOKEN","GITHUB_TOKEN"],"actions":[{"repo":"actions/cache/restore","sha":"27d5ce7f107fe9357f9df03efb73ab90386fccae","version":"v5.0.5"},{"repo":"actions/cache/save","sha":"27d5ce7f107fe9357f9df03efb73ab90386fccae","version":"v5.0.5"},{"repo":"actions/checkout","sha":"de0fac2e4500dabe0009e67214ff5f5447ce83dd","version":"v6.0.2"},{"repo":"actions/download-artifact","sha":"3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c","version":"v8.0.1"},{"repo":"actions/github-script","sha":"3a2844b7e9c422d3c10d287c895573f7108da1b3","version":"v9.0.0"},{"repo":"actions/github-script","sha":"v9","version":"v9"},{"repo":"actions/setup-node","sha":"48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e","version":"v6.4.0"},{"repo":"actions/upload-artifact","sha":"043fb46d1a93c77aae656e7c1c64a875d1fc6a0a","version":"v7.0.1"},{"repo":"github/gh-aw-actions/setup","sha":"v0.77.5","version":"v0.77.5"}],"resolution_failures":[{"repo":"actions/github-script","ref":"v9","error_type":"dynamic_resolution_failed"}],"containers":[{"image":"ghcr.io/github/gh-aw-firewall/agent:0.25.58"},{"image":"ghcr.io/github/gh-aw-firewall/api-proxy:0.25.58"},{"image":"ghcr.io/github/gh-aw-firewall/squid:0.25.58"},{"image":"ghcr.io/github/gh-aw-mcpg:v0.3.22"},{"image":"ghcr.io/github/github-mcp-server:v1.1.0"},{"image":"node:lts-alpine","digest":"sha256:d1b3b4da11eefd5941e7f0b9cf17783fc99d9c6fc34884a665f40a06dbdfc94f","pinned_image":"node:lts-alpine@sha256:d1b3b4da11eefd5941e7f0b9cf17783fc99d9c6fc34884a665f40a06dbdfc94f"}]} # ___ _ _ # / _ \ | | (_) @@ -22,7 +22,7 @@ # # For more information: https://github.github.com/gh-aw/introduction/overview/ # -# Analyze ASan/UBSan sanitizer logs from the memory-safety workflow and post findings as a GitHub Discussion. +# Analyze ASan/UBSan sanitizer logs from the memory-safety workflow and file findings as a GitHub issue. # # Frontmatter env variables: # - GH_TOKEN: (main workflow) @@ -210,21 +210,21 @@ jobs: run: | bash "${RUNNER_TEMP}/gh-aw/actions/create_prompt_first.sh" { - cat << 'GH_AW_PROMPT_413c70864e673ac4_EOF' + cat << 'GH_AW_PROMPT_0d048d29da1eafa3_EOF' - GH_AW_PROMPT_413c70864e673ac4_EOF + GH_AW_PROMPT_0d048d29da1eafa3_EOF cat "${RUNNER_TEMP}/gh-aw/prompts/xpia.md" cat "${RUNNER_TEMP}/gh-aw/prompts/temp_folder_prompt.md" cat "${RUNNER_TEMP}/gh-aw/prompts/markdown.md" cat "${RUNNER_TEMP}/gh-aw/prompts/cache_memory_prompt.md" cat "${RUNNER_TEMP}/gh-aw/prompts/safe_outputs_prompt.md" - cat << 'GH_AW_PROMPT_413c70864e673ac4_EOF' + cat << 'GH_AW_PROMPT_0d048d29da1eafa3_EOF' - Tools: create_discussion, missing_tool, missing_data, noop + Tools: create_issue, missing_tool, missing_data, noop - GH_AW_PROMPT_413c70864e673ac4_EOF + GH_AW_PROMPT_0d048d29da1eafa3_EOF cat "${RUNNER_TEMP}/gh-aw/prompts/mcp_cli_tools_prompt.md" - cat << 'GH_AW_PROMPT_413c70864e673ac4_EOF' + cat << 'GH_AW_PROMPT_0d048d29da1eafa3_EOF' The following GitHub context information is available for this workflow: {{#if github.actor}} @@ -253,12 +253,12 @@ jobs: {{/if}} - GH_AW_PROMPT_413c70864e673ac4_EOF + GH_AW_PROMPT_0d048d29da1eafa3_EOF cat "${RUNNER_TEMP}/gh-aw/prompts/github_mcp_tools_with_safeoutputs_prompt.md" - cat << 'GH_AW_PROMPT_413c70864e673ac4_EOF' + cat << 'GH_AW_PROMPT_0d048d29da1eafa3_EOF' {{#runtime-import .github/workflows/memory-safety-report.md}} - GH_AW_PROMPT_413c70864e673ac4_EOF + GH_AW_PROMPT_0d048d29da1eafa3_EOF } > "$GH_AW_PROMPT" - name: Interpolate variables and render templates uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 @@ -356,7 +356,6 @@ jobs: permissions: actions: read contents: read - discussions: read issues: read pull-requests: read concurrency: @@ -503,40 +502,49 @@ jobs: mkdir -p "${RUNNER_TEMP}/gh-aw/safeoutputs" mkdir -p /tmp/gh-aw/safeoutputs mkdir -p /tmp/gh-aw/mcp-logs/safeoutputs - cat > "${RUNNER_TEMP}/gh-aw/safeoutputs/config.json" << 'GH_AW_SAFE_OUTPUTS_CONFIG_a51ec95cdbf8205c_EOF' - {"create_discussion":{"category":"agentic workflows","close_older_discussions":true,"expires":168,"fallback_to_issue":true,"max":1,"title_prefix":"[Memory Safety] "},"create_report_incomplete_issue":{},"max_bot_mentions":1,"mentions":{"enabled":false},"missing_data":{},"missing_tool":{},"noop":{"max":1,"report-as-issue":"false"},"report_incomplete":{}} - GH_AW_SAFE_OUTPUTS_CONFIG_a51ec95cdbf8205c_EOF + cat > "${RUNNER_TEMP}/gh-aw/safeoutputs/config.json" << 'GH_AW_SAFE_OUTPUTS_CONFIG_c9563548363f5229_EOF' + {"create_issue":{"labels":["bug","memory-safety","automated-analysis"],"max":1,"title_prefix":"[Memory Safety] "},"create_report_incomplete_issue":{},"max_bot_mentions":1,"mentions":{"enabled":false},"missing_data":{},"missing_tool":{},"noop":{"max":1,"report-as-issue":"false"},"report_incomplete":{}} + GH_AW_SAFE_OUTPUTS_CONFIG_c9563548363f5229_EOF - name: Generate Safe Outputs Tools env: GH_AW_TOOLS_META_JSON: | { "description_suffixes": { - "create_discussion": " CONSTRAINTS: Maximum 1 discussion(s) can be created. Title will be prefixed with \"[Memory Safety] \". Discussions will be created in category \"agentic workflows\"." + "create_issue": " CONSTRAINTS: Maximum 1 issue(s) can be created. Title will be prefixed with \"[Memory Safety] \". Labels [\"bug\" \"memory-safety\" \"automated-analysis\"] will be automatically added." }, "repo_params": {}, "dynamic_tools": [] } GH_AW_VALIDATION_JSON: | { - "create_discussion": { + "create_issue": { "defaultMax": 1, "fields": { "body": { "required": true, "type": "string", "sanitize": true, - "maxLength": 65000, - "minLength": 64 + "maxLength": 65000 }, - "category": { - "type": "string", - "sanitize": true, - "maxLength": 128 + "fields": { + "type": "array" + }, + "labels": { + "type": "array", + "itemType": "string", + "itemSanitize": true, + "itemMaxLength": 128 + }, + "parent": { + "issueOrPRNumber": true }, "repo": { "type": "string", "maxLength": 256 }, + "temporary_id": { + "type": "string" + }, "title": { "required": true, "type": "string", @@ -704,7 +712,7 @@ jobs: mkdir -p /home/runner/.copilot GH_AW_NODE=$(which node 2>/dev/null || command -v node 2>/dev/null || echo node) - cat << GH_AW_MCP_CONFIG_d1c0e6d43d005b0a_EOF | "$GH_AW_NODE" "${RUNNER_TEMP}/gh-aw/actions/start_mcp_gateway.cjs" + cat << GH_AW_MCP_CONFIG_5e59fdbe6d1c695e_EOF | "$GH_AW_NODE" "${RUNNER_TEMP}/gh-aw/actions/start_mcp_gateway.cjs" { "mcpServers": { "github": { @@ -745,7 +753,7 @@ jobs: "payloadDir": "${MCP_GATEWAY_PAYLOAD_DIR}" } } - GH_AW_MCP_CONFIG_d1c0e6d43d005b0a_EOF + GH_AW_MCP_CONFIG_5e59fdbe6d1c695e_EOF - name: Mount MCP servers as CLIs id: mount-mcp-clis continue-on-error: true @@ -1015,7 +1023,6 @@ jobs: runs-on: ubuntu-slim permissions: contents: read - discussions: write issues: write concurrency: group: "gh-aw-conclusion-memory-safety-report" @@ -1143,8 +1150,6 @@ jobs: GH_AW_AGENTIC_ENGINE_TIMEOUT: ${{ needs.agent.outputs.agentic_engine_timeout }} GH_AW_MODEL_NOT_SUPPORTED_ERROR: ${{ needs.agent.outputs.model_not_supported_error }} GH_AW_ENGINE_API_HOSTS: "api.enterprise.githubcopilot.com,api.githubcopilot.com,api.business.githubcopilot.com,api.individual.githubcopilot.com" - GH_AW_CREATE_DISCUSSION_ERRORS: ${{ needs.safe_outputs.outputs.create_discussion_errors }} - GH_AW_CREATE_DISCUSSION_ERROR_COUNT: ${{ needs.safe_outputs.outputs.create_discussion_error_count }} GH_AW_LOCKDOWN_CHECK_FAILED: ${{ needs.activation.outputs.lockdown_check_failed }} GH_AW_STALE_LOCK_FILE_FAILED: ${{ needs.activation.outputs.stale_lock_file_failed }} GH_AW_GROUP_REPORTS: "false" @@ -1258,7 +1263,7 @@ jobs: uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 env: WORKFLOW_NAME: "Memory Safety Analysis Report Generator" - WORKFLOW_DESCRIPTION: "Analyze ASan/UBSan sanitizer logs from the memory-safety workflow and post findings as a GitHub Discussion." + WORKFLOW_DESCRIPTION: "Analyze ASan/UBSan sanitizer logs from the memory-safety workflow and file findings as a GitHub issue." HAS_PATCH: ${{ needs.agent.outputs.has_patch }} with: script: | @@ -1421,7 +1426,6 @@ jobs: runs-on: ubuntu-slim permissions: contents: read - discussions: write issues: write timeout-minutes: 15 env: @@ -1440,6 +1444,8 @@ jobs: code_push_failure_errors: ${{ steps.process_safe_outputs.outputs.code_push_failure_errors }} create_discussion_error_count: ${{ steps.process_safe_outputs.outputs.create_discussion_error_count }} create_discussion_errors: ${{ steps.process_safe_outputs.outputs.create_discussion_errors }} + created_issue_number: ${{ steps.process_safe_outputs.outputs.created_issue_number }} + created_issue_url: ${{ steps.process_safe_outputs.outputs.created_issue_url }} process_safe_outputs_processed_count: ${{ steps.process_safe_outputs.outputs.processed_count }} process_safe_outputs_temporary_id_map: ${{ steps.process_safe_outputs.outputs.temporary_id_map }} steps: @@ -1489,7 +1495,7 @@ jobs: GH_AW_ALLOWED_DOMAINS: "api.business.githubcopilot.com,api.enterprise.githubcopilot.com,api.github.com,api.githubcopilot.com,api.individual.githubcopilot.com,api.snapcraft.io,archive.ubuntu.com,azure.archive.ubuntu.com,crl.geotrust.com,crl.globalsign.com,crl.identrust.com,crl.sectigo.com,crl.thawte.com,crl.usertrust.com,crl.verisign.com,crl3.digicert.com,crl4.digicert.com,crls.ssl.com,github.com,host.docker.internal,json-schema.org,json.schemastore.org,keyserver.ubuntu.com,ocsp.digicert.com,ocsp.geotrust.com,ocsp.globalsign.com,ocsp.identrust.com,ocsp.sectigo.com,ocsp.ssl.com,ocsp.thawte.com,ocsp.usertrust.com,ocsp.verisign.com,packagecloud.io,packages.cloud.google.com,packages.microsoft.com,ppa.launchpad.net,raw.githubusercontent.com,registry.npmjs.org,s.symcb.com,s.symcd.com,security.ubuntu.com,telemetry.enterprise.githubcopilot.com,ts-crl.ws.symantec.com,ts-ocsp.ws.symantec.com,www.googleapis.com" GITHUB_SERVER_URL: ${{ github.server_url }} GITHUB_API_URL: ${{ github.api_url }} - GH_AW_SAFE_OUTPUTS_HANDLER_CONFIG: "{\"create_discussion\":{\"category\":\"agentic workflows\",\"close_older_discussions\":true,\"expires\":168,\"fallback_to_issue\":true,\"max\":1,\"title_prefix\":\"[Memory Safety] \"},\"create_report_incomplete_issue\":{},\"mentions\":{\"enabled\":false},\"missing_data\":{},\"missing_tool\":{},\"noop\":{\"max\":1,\"report-as-issue\":\"false\"},\"report_incomplete\":{}}" + GH_AW_SAFE_OUTPUTS_HANDLER_CONFIG: "{\"create_issue\":{\"labels\":[\"bug\",\"memory-safety\",\"automated-analysis\"],\"max\":1,\"title_prefix\":\"[Memory Safety] \"},\"create_report_incomplete_issue\":{},\"mentions\":{\"enabled\":false},\"missing_data\":{},\"missing_tool\":{},\"noop\":{\"max\":1,\"report-as-issue\":\"false\"},\"report_incomplete\":{}}" with: github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }} script: | diff --git a/.github/workflows/memory-safety-report.md b/.github/workflows/memory-safety-report.md index 56ffe514f..0e8464471 100644 --- a/.github/workflows/memory-safety-report.md +++ b/.github/workflows/memory-safety-report.md @@ -1,7 +1,7 @@ --- description: > Analyze ASan/UBSan sanitizer logs from the memory-safety workflow - and post findings as a GitHub Discussion. + and file findings as a GitHub issue. on: workflow_run: @@ -16,7 +16,6 @@ timeout-minutes: 30 permissions: actions: read contents: read - discussions: read issues: read pull-requests: read @@ -35,11 +34,10 @@ safe-outputs: mentions: false allowed-github-references: [] max-bot-mentions: 1 - create-discussion: + create-issue: title-prefix: "[Memory Safety] " - category: "Agentic Workflows" - close-older-discussions: true - expires: 7d + labels: [bug, memory-safety, automated-analysis] + max: 1 missing-tool: create-issue: true noop: @@ -111,9 +109,9 @@ Check cache memory for previous run results: - List of previously known issues - Identify new findings (regressions) vs. resolved findings (improvements) -### 4. Generate the Discussion Report +### 4. Generate the Issue Report -Create a GitHub Discussion. Use `###` or lower for section headers, never `##` or `#`. Wrap verbose sections in `
` tags to keep the report scannable. +Create a GitHub issue using `create-issue`. Use `##` or lower for section headers and wrap verbose sections in `
` tags to keep the report scannable. ```markdown **Date**: YYYY-MM-DD @@ -190,7 +188,7 @@ Create a GitHub Discussion. Use `###` or lower for section headers, never `##` o
``` -If zero findings across all tools, create a discussion noting a clean run with the commit and workflow run link. +If zero findings across all tools, call `noop` and include a clean-run summary (commit and workflow run link) in the no-op message. ### 5. Update Cache Memory @@ -203,7 +201,7 @@ Store the current run's results in cache memory for future comparison: - If the triggering workflow failed entirely, report that analysis could not complete and include any partial results. - If no artifacts are available, report that and suggest running the workflow manually. -- If the helper scripts fail, report the error in the discussion body and stop. +- If the helper scripts fail, report the error in the issue body and stop. ## Guidelines @@ -217,6 +215,6 @@ Store the current run's results in cache memory for future comparison: - DO NOT create pull requests or modify source files. - DO NOT attempt to fix the findings automatically. -- DO close older Memory Safety discussions automatically (configured via `close-older-discussions: true`). +- DO create issues only when there are actionable findings; use `noop` for clean runs. - DO always report the commit SHA so findings can be correlated with specific code versions. - DO use cache memory to track trends over multiple runs. \ No newline at end of file From 353131c7f0d0d916cc24c71e6c2b5ea974ee947b Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Mon, 8 Jun 2026 23:24:02 -0700 Subject: [PATCH 08/14] Publish generated SMT2 outputs in FStar master build discussions (#9790) This updates `fstar-master-build.yml` so generated `.smt2` files are preserved and discoverable from the build discussion. The discussion now links the artifact and includes an inline preview of each generated SMT2 file (first 1000 lines). - **SMT2 collection and packaging** - Added an always-run step to recursively find generated `*.smt2` files under the FStar checkout. - Copies discovered files into a dedicated artifact staging directory while preserving relative paths. - **Artifact publication** - Added artifact upload for collected SMT2 files (`fstar-generated-smt2-${{ github.run_id }}`). - Exposes uploaded artifact metadata to downstream steps for linking. - **Discussion enrichment** - Extended discussion body generation to include: - direct artifact link (when SMT2 files exist), - inline preview blocks with the first 1000 lines per file, - fallback messaging when no SMT2 files are produced. - Added size-aware truncation to keep discussion content within GitHub body limits. ```yaml - name: Upload generated SMT2 artifact id: upload_smt2 if: always() && steps.collect_smt2.outputs.has_files == 'true' uses: actions/upload-artifact@v4 with: name: fstar-generated-smt2-${{ github.run_id }} path: /tmp/gh-aw/agent/smt2-artifact ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- .github/workflows/fstar-master-build.yml | 72 ++++++++++++++++++++++++ 1 file changed, 72 insertions(+) diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml index f5b9417f2..02a2767d4 100644 --- a/.github/workflows/fstar-master-build.yml +++ b/.github/workflows/fstar-master-build.yml @@ -107,12 +107,60 @@ jobs: test -x /tmp/gh-aw/agent/FStar/out/bin/fstar.exe || { echo "Error: FStar binary not found or not executable at /tmp/gh-aw/agent/FStar/out/bin/fstar.exe"; exit 1; } /tmp/gh-aw/agent/FStar/out/bin/fstar.exe --version | tee /tmp/gh-aw/agent/fstar-version.txt + - name: Collect generated SMT2 files + id: collect_smt2 + if: always() + run: | + set -euo pipefail + rm -rf /tmp/gh-aw/agent/smt2-artifact + mkdir -p /tmp/gh-aw/agent/smt2-artifact + SMT2_PREVIEW=/tmp/gh-aw/agent/smt2-preview.md + SMT2_HEAD_LINES=1000 + > "$SMT2_PREVIEW" + + if [ -d /tmp/gh-aw/agent/FStar ]; then + mapfile -t SMT2_FILES < <(find /tmp/gh-aw/agent/FStar -type f -name '*.smt2' | sort) + else + SMT2_FILES=() + fi + + if [ "${#SMT2_FILES[@]}" -eq 0 ]; then + echo "has_files=false" >> "$GITHUB_OUTPUT" + exit 0 + fi + + for file in "${SMT2_FILES[@]}"; do + rel="${file#/tmp/gh-aw/agent/FStar/}" + target="/tmp/gh-aw/agent/smt2-artifact/${rel}" + mkdir -p "$(dirname "$target")" + cp "$file" "$target" + { + printf '#### `%s`\n\n' "$rel" + printf '```smt2\n' + head -n "$SMT2_HEAD_LINES" "$file" + printf '\n```\n\n' + } >> "$SMT2_PREVIEW" + done + + echo "has_files=true" >> "$GITHUB_OUTPUT" + + - name: Upload generated SMT2 artifact + id: upload_smt2 + if: always() && steps.collect_smt2.outputs.has_files == 'true' + uses: actions/upload-artifact@v4 + with: + name: fstar-generated-smt2-${{ github.run_id }} + path: /tmp/gh-aw/agent/smt2-artifact + if-no-files-found: error + retention-days: 7 + - name: Create discussion summary if: always() uses: actions/github-script@v9 env: RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }} FSTAR_BUILD_OUTCOME: ${{ steps.build_fstar.outcome }} + SMT2_ARTIFACT_ID: ${{ steps.upload_smt2.outputs.artifact-id }} with: script: | const fs = require('fs'); @@ -128,6 +176,28 @@ jobs: const fstarStatus = fstarBuildSucceeded ? '✅ FStar build completed' : `⚠️ FStar build ${fstarBuildOutcome} (pipeline continued)`; + const smt2ArtifactId = (process.env.SMT2_ARTIFACT_ID || '').trim(); + const smt2ArtifactUrl = smt2ArtifactId ? `${process.env.RUN_URL}/artifacts/${smt2ArtifactId}` : ''; + const smt2PreviewFile = '/tmp/gh-aw/agent/smt2-preview.md'; + const maxPreviewChars = 55000; // Keep below GitHub's 65536-character discussion body limit, leaving room for non-preview sections. + let smt2Preview = readIfExists(smt2PreviewFile) ?? ''; + const smt2PreviewChars = Array.from(smt2Preview); + if (smt2PreviewChars.length > maxPreviewChars) { + smt2Preview = `${smt2PreviewChars.slice(0, maxPreviewChars).join('')}\n\n... (truncated due to discussion size limits)`; + } + const smt2Section = smt2ArtifactId + ? [ + `### Generated SMT2 files`, + `- Artifact: ${smt2ArtifactUrl}`, + ``, + `First 1000 lines per generated \`.smt2\` file:`, + ``, + smt2Preview || '_No preview content available._' + ].join('\n') + : [ + `### Generated SMT2 files`, + `- No generated \`.smt2\` files were found.` + ].join('\n'); const date = new Date().toISOString().slice(0, 10); const owner = context.repo.owner; @@ -171,6 +241,8 @@ jobs: `- FStar: \`${fstarVersionText}\``, `- FStar commit: \`${fstarCommit}\``, ``, + smt2Section, + ``, `### Run`, `- Workflow run: ${process.env.RUN_URL}` ].join('\n'); From 32e50e014ee2549dad5e725b6173404bccb4f665 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 Jun 2026 06:58:11 -0700 Subject: [PATCH 09/14] Update default fstar_otherflags for build workflow --- .github/workflows/fstar-master-build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml index 02a2767d4..8d347be5d 100644 --- a/.github/workflows/fstar-master-build.yml +++ b/.github/workflows/fstar-master-build.yml @@ -28,7 +28,7 @@ on: fstar_otherflags: description: "Extra FStar OTHERFLAGS" required: false - default: "--split_queries --log_failing_queries --ext higher_order_smt --proof_recovery" + default: "--split_queries on_failure --log_failing_queries --ext higher_order_smt --proof_recovery" discussion_category: description: Discussion category name required: false From a5495b78fa1610bad5484a3d953953d8ea77cd39 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 9 Jun 2026 07:36:05 -0700 Subject: [PATCH 10/14] Avoid invalidated column-cell references in LP pivot paths (#9783) MSVC ASan reports showed a container-overflow in LP tableau pivoting, reproducible from both examples and solver tests (issue #9781). The failure came from reading a `column_cell` through a reference after pivoting removed that entry from the backing column. - **Root cause** - `pivot_column_tableau` and the analogous Diophantine elimination loop both held `auto& c = column.back()` across a call (`pivot_row_to_row_given_cell`) that immediately removes that very cell from the column via `remove_element`. - After the mutation, the subsequent read `c.var()` used for bookkeeping observed invalid memory. - **Change** - Record the affected row in the bookkeeping set (`m_touched_rows` / `m_changed_rows`) by reading `c.var()` **before** the pivot call, while the back cell is still valid. - Make `static_matrix::pivot_row_to_row_given_cell` return `void` instead of `bool`. Its result (`!rowii.empty()`) was always `true`: both callers keep the matrix at full row rank (the tableau basis columns form an identity submatrix; the Diophantine `m_l_matrix` stays invertible), so an elementary row operation can never empty a row. The dead `if (!...) return false;` early-exit in `pivot_column_tableau` is removed and replaced with a `SASSERT(!rowii.empty())` documenting the invariant. - **Affected code paths** - `src/math/lp/static_matrix.h`, `src/math/lp/static_matrix.cpp`, `src/math/lp/static_matrix_def.h` - `src/math/lp/lp_core_solver_base_def.h` - `src/math/lp/dioph_eq.cpp` - **Behavioral impact** - No algorithmic change to pivoting. - Removes the stale-reference hazard in the loops that repeatedly eliminate entries from a column. ```c++ while (column.size() > 1) { auto& c = column.back(); SASSERT(c.var() != piv_row_index); if (m_touched_rows != nullptr) m_touched_rows->insert(c.var()); m_A.pivot_row_to_row_given_cell(piv_row_index, c, j); } ``` - **Verification** - Reproduced the exact issue #9781 failure on a local ASan build (`container-overflow` in `pivot_column_tableau`) using the pre-fix code, and confirmed it is gone with this change. - The 4 reported tests pass clean under ASan: `c_example`, `cpp_example`, `test-z3 get_implied_equalities`, `test-z3 quant_solve`. - Full `test-z3 /a` suite: 89 passed, 0 failed, 0 ASan errors. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner Co-authored-by: Lev Nachmanson Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/dioph_eq.cpp | 2 +- src/math/lp/lp_core_solver_base_def.h | 8 +++----- src/math/lp/static_matrix.cpp | 4 ++-- src/math/lp/static_matrix.h | 2 +- src/math/lp/static_matrix_def.h | 4 ++-- 5 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 5058bfaf3..0b3c5166a 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -709,8 +709,8 @@ namespace lp { while (column.size() > 1) { auto& c = column.back(); SASSERT(c.var() != last_row_index); - m_l_matrix.pivot_row_to_row_given_cell(last_row_index, c, j); m_changed_rows.insert(c.var()); + m_l_matrix.pivot_row_to_row_given_cell(last_row_index, c, j); } } diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index c4c41c26e..21bd48a22 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -277,13 +277,11 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) { m_A.m_rows[c.var()][c.offset()].offset() = pivot_col_cell_index; } while (column.size() > 1) { - auto & c = column.back(); + auto& c = column.back(); SASSERT(c.var() != piv_row_index); - if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) { - return false; - } - if (m_touched_rows!= nullptr) + if (m_touched_rows != nullptr) m_touched_rows->insert(c.var()); + m_A.pivot_row_to_row_given_cell(piv_row_index, c, j); } if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs) diff --git a/src/math/lp/static_matrix.cpp b/src/math/lp/static_matrix.cpp index 26ce218de..4abf0d88a 100644 --- a/src/math/lp/static_matrix.cpp +++ b/src/math/lp/static_matrix.cpp @@ -51,8 +51,8 @@ namespace lp { template void static_matrix >::set(unsigned int, unsigned int, mpq const&); - template bool static_matrix::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int); - template bool static_matrix >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int); + template void static_matrix::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int); + template void static_matrix >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int); template void static_matrix >::pivot_row_to_row_given_cell_with_sign(unsigned int, column_cell&, unsigned int, int); template void static_matrix::pivot_row_to_row_given_cell_with_sign(unsigned int, row_cell&, unsigned int, int); template void static_matrix >::add_rows(mpq const&, unsigned int, unsigned int); diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index 415d3f1a2..08db2245d 100644 --- a/src/math/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -293,7 +293,7 @@ public: // pivot row i to row ii - bool pivot_row_to_row_given_cell(unsigned i, column_cell& c, unsigned j); + void pivot_row_to_row_given_cell(unsigned i, column_cell& c, unsigned j); void pivot_row_to_row_given_cell_with_sign(unsigned piv_row_index, column_cell& c, unsigned j, int j_sign); void transpose_rows(unsigned i, unsigned ii) { auto t = m_rows[i]; diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h index b28d67740..af07c4482 100644 --- a/src/math/lp/static_matrix_def.h +++ b/src/math/lp/static_matrix_def.h @@ -48,7 +48,7 @@ namespace lp { } - template bool static_matrix::pivot_row_to_row_given_cell(unsigned i, + template void static_matrix::pivot_row_to_row_given_cell(unsigned i, column_cell & c, unsigned pivot_col) { unsigned ii = c.var(); SASSERT(i < row_count() && ii < column_count() && i != ii); @@ -82,7 +82,7 @@ namespace lp { if (is_zero(rowii[k].coeff())) remove_element(rowii, rowii[k]); } - return !rowii.empty(); + SASSERT(!rowii.empty()); } From 6eeb274cd22a4d53990732233e382ca282aaa857 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Tue, 9 Jun 2026 10:22:03 -0700 Subject: [PATCH 11/14] Fix FPA incremental soundness for fp.to_* terms (#9022) (#9787) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #9022. ## Problem After a `(push)`, Z3 could incorrectly report `unsat` for satisfiable FPA formulas in which an uninterpreted function returns a floating-point value (e.g. `int_to_fp`). The example in #9022 has a single `push` and a single `check-sat` (no `pop`), so the `m_rw.reset()` added in `pop_scope_eh` by #8712 does not apply. ## Root cause `theory_fpa` lazily converts FP constraints to bit-vectors and asserts the equivalences/side conditions as **unit theory axioms** (`assert_cnstr` → `mk_th_axiom`, which `assign`s the literal at the current decision level). For `fp.to_*` terms (`fp.to_real`, `fp.to_ubv`, …) the conversion equality and side conditions are emitted **only** in `internalize_term()`, which runs exactly once. The `else if` branch for fpa-family conversion terms in `relevant_eh` previously did nothing. These unit axioms are level-local: on DPLL backtracking the assignment is undone, but `internalize_term()` is not re-run for the already-internalized term (in particular when the term lives at the user-`push` base level, where its clause is not a reinit clause). The side conditions include the axioms linking FP uninterpreted functions to their bit-vector counterparts (`int_to_fp(i) = fp(extract(int_to_fp_bv(i)))`). Once lost, `int_to_fp_bv` becomes unconstrained, enabling an unsound `unsat`. This is exactly the behavior described in #8345/#9022 (and why the result flips with vs. without `push`). ## Fix `relevant_eh` re-fires on relevancy re-propagation after a backtrack. Re-emit the conversion equality and side conditions for `fp.to_*` terms there, mirroring `internalize_term`, so the FP↔BV linking axioms stay in force across backtracking. On an `m_conversions` cache hit this just re-asserts the (hash-consed) conversion equality and a `true` side condition, so it adds no new terms and no clause bloat. The change only adds sound constraints, so it can never turn a satisfiable formula `unsat`. ## Validation - #9022 reproducer: no longer reports `unsat` across many random seeds and longer timeouts; a model (`sat`) is still found (the problem is inherently hard quantified FP + nonlinear arithmetic, so timeouts are expected). - #8345 reproducer: first `check-sat` still `unsat` (the negated quantifier axiom is valid). - Additional incremental push/pop FP cases with `fp.to_real`/`fp.add`/`fp.sub` and FP-returning UFs: correct, consistent results. - `test-z3 /a`: all 89 unit tests pass. - Debug build (soundness assertions enabled): no assertion failures on the above cases. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/smt/theory_fpa.cpp | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 107456455..492595f60 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -494,6 +494,31 @@ namespace smt { else if (is_app(n) && to_app(n)->get_family_id() == get_family_id()) { // These are the conversion functions fp.to_* */ SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n)); + + // The conversion equality and side conditions for fp.to_* terms are + // emitted in internalize_term(), which runs exactly once. Those are + // asserted as theory axioms at the current decision level and are + // undone on DPLL backtracking, while internalize_term() is not run + // again for the already-internalized term (e.g. when the term lives + // at the user push base level and its clause is not reinitialized). + // The side conditions include the axioms linking FP uninterpreted + // functions to their bit-vector counterparts; losing them leaves the + // BV counterpart unconstrained and causes an incremental-mode + // soundness bug. relevant_eh re-fires on relevancy re-propagation + // after a backtrack, so re-emit them here to keep them in force. + switch ((fpa_op_kind)to_app(n)->get_decl_kind()) { + case OP_FPA_TO_FP: + case OP_FPA_TO_UBV: + case OP_FPA_TO_SBV: + case OP_FPA_TO_REAL: + case OP_FPA_TO_IEEE_BV: { + expr_ref conv = convert(n); + assert_cnstr(m.mk_eq(n, conv)); + assert_cnstr(mk_side_conditions()); + break; + } + default: /* ignore */; + } } else { /* Theory variables can be merged when (= bv-term (bvwrap fp-term)), From f0956a622f32f013803d12b2a01dbc2fb3a1e37c Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 9 Jun 2026 13:42:28 -0700 Subject: [PATCH 12/14] Refactor regex subset logic into `seq_subset` with depth-bounded recursion and optimized concat traversal (#9777) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `seq_rewriter::is_subset` was too localized and missed key subset implications for regex concatenations. This change extracts subset reasoning into a dedicated component and adds heuristic closure/monotonicity rules, then tunes the recursion strategy based on profiling feedback. - **Architecture: isolate subset reasoning** - Introduce `seq_subset` in `src/ast/rewriter` (`seq_subset.h/.cpp`). - Add `seq_subset` as an attribute on `seq_rewriter` and route `seq_rewriter::is_subset` through it. - Keep `seq_rewriter` focused on rewrite orchestration while subset logic evolves independently. - **Subset rules: broaden inferable cases** - Add derive-style subset decomposition across `union`, `intersection`, `complement`, `concat`, and bounded `loop`. - Add E3-style closure rules: - `R ⊆ R*` - `R1* ⊆ R2* ⇐ R1 ⊆ R2` - `R1+ ⊆ R2+ ⇐ R1 ⊆ R2` - Add missing cheap cases: - `ε ⊆ R` when `R` is nullable - `R ⊆ R+` - `R+ ⊆ R*` - Range containment: `[c1–c2] ⊆ [c3–c4]` when `c3 ≤ c1 ∧ c2 ≤ c4` - `to_re(s) ⊆ range` for single-character string constants - Difference monotonicity: `a1 \ a2 ⊆ b` when `a1 ⊆ b` - Star absorption checks for concat/star combinations (`R·R* ⊆ R*`, `R*·R ⊆ R*`) - Preserve nullable-based `. +` handling and top/bottom regular-language shortcuts. - **Concatenation reasoning and traversal tuning** - Remove `flatten_concat` and assume right-associative concatenation traversal. - Keep containment shortcuts for both `R ⊆ Σ*·R'` and `R ⊆ R'·Σ*` when `R ⊆ R'`. - Make concat/concat handling tail-recursive on second arguments. - **Depth-bounded recursion (profiling follow-up)** - Replace visited-pair hash-table recursion state with an explicit depth parameter in `is_subset_rec`. - Add `m_max_depth = 3` and return `false` when the bound is reached. - Increment depth on recursive calls, except for the tail-recursive concat-second-argument step. - **Build integration** - Register `seq_subset.cpp` in `src/ast/rewriter/CMakeLists.txt`. ```cpp // seq_rewriter.cpp bool seq_rewriter::is_subset(expr* r1, expr* r2) const { return m_subset.is_subset(r1, r2); } ``` --------- Signed-off-by: Nikolaj Bjorner Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- gmon.out | Bin 0 -> 14458562 bytes src/ast/rewriter/CMakeLists.txt | 1 + src/ast/rewriter/seq_rewriter.cpp | 47 +--------- src/ast/rewriter/seq_rewriter.h | 5 +- src/ast/rewriter/seq_subset.cpp | 146 ++++++++++++++++++++++++++++++ src/ast/rewriter/seq_subset.h | 30 ++++++ 6 files changed, 181 insertions(+), 48 deletions(-) create mode 100644 gmon.out create mode 100644 src/ast/rewriter/seq_subset.cpp create mode 100644 src/ast/rewriter/seq_subset.h diff --git a/gmon.out b/gmon.out new file mode 100644 index 0000000000000000000000000000000000000000..cba10a19b2a99a2517d591f2bf1b928974a77eb5 GIT binary patch literal 14458562 zcmeFtu?>JA5Cu?Nz$Jm$C=@KfPLAMW7!&B+;9YZX&b6Hv7{Tx6L3X3p{#SjJsL5m zd(GtLw`#oTtt7o_pGJ8u8-On`dkeH0$ki8}ZVQom%I<7l-H7 z(`+Wky*TT|!ROS?&;8;0^?2=_>>@twef6>_x6$~{?PQ7TyVRJs=CzKSFFv=%cYj@_ zD{*z#cJrS*)RWmg+s(^mv*^WDFAl!2v-vdQU;fG|x>;{>6YyNov)((-Y+m9#;vIkO^wE2h%QLYc4<1&R zl(*)cj!T++d5w8DyzVj1Bjycvi(_2&;wEBV3}tfo@b*9@t{zci?z1duc0rA)RO0TD zHQx3c>(}4@w8PO?@y)Bh^i(TUCGtDOAxQ}067>`fove`$x_(iY3=CYZ@)5EK;b?W&j(_eK_2S|;>cp@9T)hSA(IfumTTgAi|IPYMb1jYE zR^z?ja%yt@SM{4K?@`xT_Bs0N8oxSrQ{p1x<*~F9cM+Qd%|1{!fB84nuh%~aoa`P@ zuk|bcXN?79-;0|st&@40WpW$w^Lo|@c6d{eBqOisS3bD;e%)RKE<9L~s2dZb(i_=~l#jEo_{Yc$+d6rp4%$FQDKQ4az zA9W&MgI(_!M}zumGS^w|T(grJb4ev`uGLP~bH8>Q%WJT~b=u8K97oIp70=mC>SV67 zJfSQi-ZJ)Gg>HM7cJng1ymvcU_PMxEjd>fDqpu_8fyzF2_pOu7ZM6J~ z8q>4vbM;m2K1-Zk*qIzWu@h%csWFdUHlMF*%%hh$d`)L^5i!rGJOr&GHk(g=vTmM} zMQL{?mUAEdZ0A7ppX~A|4!|WeB zaq!PIzB%3_md(d;&I$6l$D?P=XN3At8Bch5mnoCGX?+%KmbCtg8uQ%C=7Z7Q)H%@h#hp0&o=)7otj1h?^?Z3} za(!86a`3&K$@wcflatFkllxwre}6k!ly(unZ&v@X#NjL31C==VvCih>GqFDP^x|Yy zH^1!F^=p}&yuP!~eJ{>`xidNWwHjadi}h>0-6N)aiL+ju_u`@#*AeqtD*If%sUG#b zSZ|4=-)PraZuj9|wDAVzUK}ykS>pbxcCy|P{<4kbX<{ESH!pGczuU=j^!Z7B>zj)& zanXybGx5`p>s&|7&+AIu^d?8~9yxXmpB1?mrxDM& zVKw-!^A2aUJQF{1*#2Y`6Zs+Dvu<;Ui(VX@+j@?UO52FJq!On$s+0L4-qQ~^=gH~; zHRdDj8xObK$?_rXKFb-czpTcW#unw}>*UEb=39(%g)CoC<1PQJeyy9o@KeMKzu=1x z%RU_W_`gkWa@&i$Uff5_w?bu~gBR7K-}E_Oc+G(_-s_7_9X;cNA8{&yj?I>+wlEu8?uWyIob^ zQB~xK&prKPoq2C^*^BF5-1g!wV)OC-KH}B)J#|Kdm)6BMaU8L^;ieJu4S2m6UQsuH z@*mZ&<<7N;nAcLh$MxcFTQ_Sa_q{lHSDnm{Xv#jfan!rVUA)Gp)YE&(L+@2?juJ<4 zr)sX`j1Rt1oh)aR@tilEiqp6*8<4?!>w%iavOWfuBEp z^jKe`G&>XP&C!dCGqK(rXJXlW6J+_a@Jo(Y^FCrOet3+Fht>5x;PlT8ml1y~Zh^AT z?W5{sF22OUqub5Pl7*l>UiQD_; z4?i_I?ZsKdKYm1=EbE*{Y)*6en|0!Sr}sJd?M~c9yyvY>9ev-6)8DBR&6T|9#bqz9 zA~sJb8Jj1R_3w5LwCTm|nOH#fpDMod*H4}1;4Pg44I?)9_ly_CHB}C@Ju_Ku;*7ug zWv37H_WDh}Vkwh@chuNiORKm~Hdo#F_4SV0#91#cdvV>1!(XoZeE;vATIV!gYJBwc z^U*wFbAe6bWx+q*wLWtdkZCW@dvVc=%U)caiRGpH`b@mx@sVM3Cf3`i7k9n5zjr;8 zJk7HC;EOwPcqZ0&6K7)CeB6tZUYy1&s>XBHi}N$F9DQ*nmZQ)A>Hg*Mz4?G>(Tmd$ z)yeb!wtnhfuFqM-X7l~8Ov*kV5d9{j}j-b&pdjG(_Wl+vtFF{;<6W4y}0ScZ7=S7 zad3mqX^whv+>6s*ob}?O7ni-b?!`?n?s{?Gi^Fqzr`d~>UYz#gycZX}xa!4qFK&Br z*NcN2cFt(ni_06;$w!~muQxkBSgm?-bF(^;k6`6qyp7oWKEw9rb@Fxbmc2~wA~x?L zXSb-6&CieKy}0Pb@vZCTm)^TR^^`~N<@q({GgtZCW*6~-+tfcSaew!AvOFg5zqrQB z|ENCvmdU|=+R6G^(4@v@@rz#E^y1)woy{k`xah@gFAg8n+2^zum%X@+m>-Un8*cF6 z&ORr-xah@AFAg8l+2^zum%X@sMBO~!T9$PVAK8h6M|I+=7x%q5{OY=SbItD`S7UR# zk1y)P{nzz2e@cx{|NMH<-nZQ2zNyCdd|Qq6&K0pa&_3ctZ#^}c@!h|FD$bwU+2=B1 zv(I(JW}g|GeNLZN_j$Kxo;uJhVzbX>#2%SIsULM_{GZpVyD6u+@9lH=pX)@k z&vC?NpBbBdE@QG;=c>2QU2mV0Z|YZ1$P4+2=AQn{!|H_POir zGh?&Q$+z~-Jz{h2i-^rSGdBC&_4YaVw%)l%Z1y>h*z9u|u|4Fsmh+h@jRpVMb_);W*ZtaBN$S!c#( zpM&r0>~j>c+2E|^j&ZB$%{LS zpGIspUq);eKX^%J^I^nh^J&Cp^L20YO>gtTcX!Tx9@>VcYlE+aPkTt{s7xr^AI zX2j;vX7ch5-85pe&t=4BpM%Rfn-3#4n@=OQo4>kle#P_7FYkKpeSGILjQD`(*LeKt z%*nVHhd#N20D(jsDhMqNHnp8aUM&k`3AbDt$HBjy>EIQp@=d7e>; zgCDQ4dH+6Jb>cc=exy*=x&GxknTx;84G$pu->$K_7zV%7iNjtT_2Re}C%riB#aS=T zdvVc=%U)dd;_xl)X&!&xcruE3^Y5ycO^N$IsgunI8pA(rH!pAh#}S(kA2K!{K1^cr zrE#;=kA2=>_u1UUyNG$imC3>Xt&>e0MZEM6>mQcMj32yDJ);sQXErYv*fe5Z$z^hW z|3@8MuK8I{iQ_M+F+Y~9`|QP4#9U`N&^lssp#1|n2in}YE;@gLbEm^fPIeJ<^YRds zF@JVemNfXRy7?Qgx=T5U&7qzQ&&0!T=N;m$>tyb;-VM*j!w(KmCK2=8KkvBtv=?^~ z^VWR9@#yp0)B|NK>m1&p#;aa-epzSvO_EVBE+T&5=5>p^9gn^{6U#m)cd8RFzJ2|A z!Qpe>lZ^R;{<5S`#A*Faq7t`fHZS|!_2Rx4$9Haz{=UOw(8;71r=MFV-*UV9b$Fx0 zWX7jIzAou8$J1P$Unlaz#<$=5T8E#6MoiD+MRYQ{d!5W%vpfK9B7X31FFMQ&2KV^9 zlLOtE$%h~Q;A9hbl|0Z79X{4PS>LZc`VEhhgZsDfTS|OHjqkrp{kk6?4z!7w`~1w~ zIy3@@&esZ?&wZNzgP zSO2iY{j7e|Ja-Jgq20XPI~Ea}=ZC&q5dK3BcTb#HRho80y$cfHAdZ*usAy7*>E z8JoqAdy^TP$!TvgV>3DLO=fH+m%Yi1&Ez^Jo4Dz1zU@u!dXuv!Ri$R1^N0=I?i<@H zr2hQq$(<`?^zCi@vg4&VjriPnbbQz`&f_Eaygom0&LJ)%=H$B$4~r**XSMq*7ue|8 zH8#&OY-t=(X!QfWMqfegS?z3Fp%ZPbLs4olSWkEjt-rz8LvUp+L zJY#ue*hG9-9I*UO{^0xSo*?i$s%I@#^BfA^!T_GF<%~(hqa8adVSrziFuk2 zJ)Y4%HqTfl2j5>eJ3o&8x|<&kG>n+PPFCXRzt+io3@Oh?(};QWs}GdaM_`zO$%wKmlKj*%ul=A53f6mu^ z@;a}2)K`CUY=W_y?}KH$-s8UJllS?~Cw=WF#|K}lv!qLJc?voA`R$jS zy5TZj9T!-+i8H?YoX+O=`iD+@?a8SdZhd9FF7t*f`^FGzsS#O_%b?4~QUYteD+r1oUd1kVl`zB&@-`w`%t{3<5 zESQ_uCzRi=>&$1a8yt>wGK=`m->QFD;{Gk|W1od|T{uT)%$bg@?&e#C+Np0U|{(c3&@ zvw6m5^G$5t#BFb%8Jm3$K3>ng*?btW0m;~GKIv^f?QNd1*?bX`c{eOK$2#Kq?>%)B zXS`dyPb!o9m~1}g&G<+EUeB!F#8=mEngfj^Hs?O+#c40jB3^vcQwPe}taBcd&Cyq% zDxM$Dn`QAi+3a)M+dN~ldB$e*;eT{MHW8c6Gd7!VW3rLY*vRjDlNp=I<)Gf)?~K0` zp*)?fA~ydS;5K4nv&2i^J>I$!4A7h|NA{pWa#LB4hl;Y1K30WkFct^2v4ce54&6ALldXLwfma zZ5@+&yC45UnUl>^>gG8)K7J^gG51+sNM!s-d_G?u(lfsCN%h5EiPLXtmsFm$_YrgR zvZRc;c@uL<-!?ov@#W;X-(UA#U$LAy&{rKqPKHmd6M33f-T3&t8S$bYt$$eltBs6# znk8<|Y+hshnq$5asIP4z{@HWt-Lb^=i|YaMsk}}`%(wp~ZsSbyNc^kzxxh|SSA5u2m$A~r`Kzow-tm*OH~ZeHRlVs2iq61P9m?z4Ps zzK@vuEOGdgbu#x^;wWP7v&3b*PP*s|PCfNZ-dZ<5FJ73J%X=F!U;UO#ao3Cci1~WH zOir$<`^<~BJX|ay=Ji=0Ln7unOI*cMc%Ejt;WiO-^Csqx^Xly$ley0l_Yq$nge4Al zb)8L|MEtWKuYXu3XT7-S#dXHGZHF$rz6CC~`>Yq&@!3jFR?joB zUQ5@npC{&ByG$-_P-CsNH*win0C&g8xq2jAbB9Q@Z#9KNa(m#?ldPqRK)_2Q-%x4pRdk-E>k80wYW zi>qE-_u{4(x4pRQ#eFXhezddBVK2^K+fF|Bcrh#@=KHu3m%YhV#Qbls%4EiN^PjE< z%9mT^{=STO@Azn;#8t%RcX)K!%ay`%j1#na!fF@NWzT;7X_`Jmdw zd{8ZMACq~Y5(n?B`^x!os!P~+8auV2gLEMoJ^Z1Xdd^|FcBTubYS`IuZLhueC9 zW}l;odGsgZ(TQUZsK*s z=JFohrZYL~#Z@ovdU15y-adPAe7icCckQCI?ZwfkGdZ|@jm;S??^$Esn*ZnUAab&f zn73w$yNG#n{OoaZA2H=i9DHHjXFjZz&4&?l^Abn#ldybTs(09k&CM~5m=9KEGGjhi zmAHItJ$i0__~HNIr@#@PaEJOTsKiP9=%x9ATE^xFYP*=s(<}$t_u^n*kKRlUdvVl@ z<6fNf;;a|vXJWbLmuF&G{HhnnuY7E|Q(g6y^(5*mz=;3)yYlPh);fM z{fStK)4#9#%$uVeeb$TfUR?CzvKLpqxbDSGFK&Br*NgjJ9DJa2n!{ck_u`}%r@grT zKkb3)8}NwvG*ROGU+ND~|M;WzYq=OQKK7qa#YIf!MO!bMUL3@}@-d`LPJ40qY4r!a z&E&Wj=Xb7?Z~vnDwfqXu;{5u}Me&E_z04|NuCrWV+cU9D?$2yq);avb&XN`xuT%f9 zOs?P-gTYNtCJaTeSEN5KflKOMbq-8 zX}W0lS?`7~>%`sLYi#au`-pjklqC(~R~DKV5*eEp664-v#%6LFlg-g*5u2mWBj)Sm zvZUef*Tpwa(9=I`&*)A^rCG$>XNmKO7sPAuCSHABeFQ6U5tDiJ632gD5A?0^k5QB* zEh6TXT;eExlc2fXcVG84fhT=miy5xVuF;o8hmY0YOauVFK&8q+l$l3)~B3Qsz-lf zjd}EXYsRl@G{0}NjMz-BdT|-gZMpdJ``)XFc`Y?DUviWP#+sarB|iOCr~~N9EaH{7sIP*)<8U#3BEIR~^#$ZJPRHE5+#LJ(m9KmRE0^Nn z*7nC z#$>)qFL4$zU!|8gKBqm~)cnK36zoSm7x z>2aSKbF#$Ar0(;)FRfo6_=xKq_W8j2O)mb&Z*us7+TuYq=97N8LRJxTvfjiGjeS0> zeq9`|x?RMayw`C_lP{|id4ZL*Pfbsb34-{!F~Xai61yx059<&&1-n z>BYe#+RblsIHi+OFD}l+vd`%Sb@OxLroQuW^I62a$2BqUnj-yH2z;uOl|E05dk5?{e~QPJQS!y|A81DwPi#ml4ym9w_3k z#w}3drZ>6kP40V>qpzt)Z}vHk*c^SdXvlElY@&p^23OY{J1wc=}pdilZ)QusyDgmP40S=``+a6 z>pN#Oj@X>hv^P2HO)h(rtKQ_MH@WRi4rZNojv}_}jCjHIPW?{)tT(yrO|E;Bn~2Tz zx$8|1zoD+PIr=DKv(8y>a^9O<^(HsH$$f8f@PxXg=IG;y%{r&O$$4*b*_&MVCbzxG zeZY5A18_g-mKIu(Pdy})? z_LO>gsUZ*te0-1jC2Kh~ieeX7{3a}twHoc1=K^(N=N$whB+*_&K{ zs@N=P+uP@^xB0#|Ik=*uG>q6BXw;jWe5%-NzKY4bYuC5c5%bPfuH^BL*CjP~u1UmZ zpVNrVy<^s!T=(L>w|U0qK*Lo}DPl9ZiI}HZ&S>+Rx_R@{>RrTU^TAKl$>yik8JnM0 zk7BZU_#H>g4|B@Vr@hJ1Pu2syHvaHC?sojI$s*=HOC0`GoxC8{dyn!-RK#ZS%ZT}d zm2&h|#O9OdUBm`t@Y;HyW}l;o4M@fYWFC{b_;U2YPuG3swNxIx=MnShxg;uCg#yg-2O~GQ0}uFeIGIRS>o_#>tyb;iMh`b7yqqJ=Dp(?hk7#ng*KMS@s%~^ zFJqL+X~g_xj1m_SQ|b7b%*irhUN$AJBj$&qW%JFM%}d<9p&mUy!2I~<9ImC+Z`GI= z*cHdiW*adNRO04$>*U3;n-X^s^NdOyzoky*8I?GETYL0(9G>-0hVN>R{+45$yt|#e z)A8K5@2m0Rx7M$pbBz0ldGr#;e^V#&=p`=S-){ck<88E#n46cli9;iq#BEIGI?InCGUhtVFNJ^E#F?Vo!*(Ckbsk2af(aoODB z@CbOakC=4z=>JsrnTsz!8QDk7#Wyh*U*h0Hb@N%eYy|}n;{b(lNbKU8%{mCj~ZeHH;&ErFy=G@m2bDcLX7wxCledcShvibN1HRe9c zlBT^l`;1u9uzoF%46Ae7_=dwy5C7#tjd}EP?xP#mmyco6-FNuAYxS7_;RJ!N!cHcg>#=JSo?LK{cjrrem zmCXki*ZAi9)O8+S9UOkT8ZrMtlQKD;wUfVeT+;9x+W0HSxQm!)R5suD;`9lfB@Lh0 z#%CVxoF~gC)tIMw*W)@zm$b25V9SVkn&%xS2jAH4vn*-ei<@5D_2THsvCq|G4u=>F z%0534<8L!4ahj8-Vk+I}7^hFIlTBQ8 z<2TpI=CT=lODE3fH70Voz-HgpncPNfjy`@yXL8ny^JjG?$KO?Bg1r3j%y+Wr#Z|;q zDmTYE;`wohsJGFg-DkP#CNHQl7hkTr!He3-*B*~PiFjV@yDVuQ@o90#EeG11*}Pn| zoA0jsY~;r;tMOegtY6Dy#@EGe>NOve`Ge{Dz!EWkk*~yc#5>3D?lm!gC|}|>Ci6XP z6Z1i}#9d708`~0BFRzPkCf5<0eQtV_+ur2$!^`T?n*(KRC%?B&rhHlaycf5< zIDSRvG$*|{?ZsKd8{fI^rXKwt>Ng+!i@P5mR}S~}+g{xF z;$UBw)EsEoi{oCLM7;ccr_N~Ai-Ujc9B9;w<6fNh;w)lw^v#Fsfj;nrBU(uE_-p^i`!lt{A+JXy*TN`c`q(|aovl%UR-{p zb8D`9ao>yMkJrsFic7NG5i(wRx6i%ihFhQe`0`Eu%jWgXUBvvC%}d-x%zxRu#KDc~ z<{$XWdTW+Air8#E>BU)Z^LfPlH|fegr#I=Wa~`o-(jsDW^i^+i(~G;_=7XEoqc;Z{ zMr;l=?!{?u^LfPPG&42_ntx{J+?NrX$yG0IdU4l_`(7O0s&nq+UYz#gEMlXy=uIvo zHXyr*_lldPyk1)0p#!ps*nsRJHb>w0;_!}jpUvbrVzbXlZ*ms#?eRceF4{$J^Hndd zd;8q>;yz+?j~m{pF20H5i0zUhHmAAj#dXBy=GZ>2BfpQ>C=D;_dG_KoVzc?I7Z<&_ z>cvgO<}`P`IQY8GI!C=YiP#{|dXtNY%^9tFaovmC-ahvc^MypYz=n_SEPmXJ(_WnQ z;-VK~O$^JT<_ zZXNM=o^@(+7qNLZ+(&Et|Q+3g{R^s zVtSU%cMiroo_mR-C)9oA=H=Wc5gYkw#N20@ocH3QxB03UH@&#)?Q`(Ny3S@v zqlnFt#=XgDFV1?KFM5-!UR?L$wioxkICxU;jCyerv3XS7M7;X%>*sal=GaC2(T{cF zYfnx+2<&^48Jo$$C3T(oiCH<&x)(RSxQp0aVEc&8tvUF{dZ4^M%YAbfj~&hCgJ<{X zBIf30oulsL^Xul#KF7T{jo7Sn){Bc?T=n9*7q=0c#b<0T?_FI{`ZBO%f$2r+YOpp=>uV~M`#8EF!dU4u|^Ilv=OuBNQ zb#HRhi@RPNT;5syuouU@IEk3IQCZUPC+j|+{+W*~Z*a@!^ZSTTyIGC5J9XOdHaw(2_aomfOUfkWh9wR3>M=IPb+pFHUY*5A@te)N?Nf8s4fs_Yz0FIDUSe{JWP|!r^i8vxvFQ z(J>A#t&{ir#X4C$rxA1W@))v=m>~6mC1U>9_hs|R3+g`er-3CduBb78wWf(Leae42 zEGGVfnpI5ZI?Lp`7l*%C_j${&Ii)m-c`;^86a^>s2AU-$VdoptUa=H0Na z^S{^0W=YFl9R6D8K)ZTN9vfO8hi(Xtue9uSgZpu36Cw21#shjuWvKLpqxbDSGFYY5=`nAxOFn+;&b5r# z+zm6{^7Q8Gn9MV(i;wuQ*{Qz~Wq8AS^w<5wsjF^zqZ$*rY(BqPJ6Rs6ceiXOOWfbO z#=L9a<^X*%xJ`{$4C?J(_Bo5#Os*onX*fIHM1!*V`nGlRyyi>XMa*Z|@?<)`U7gG) zz8Xh0=5t&V^O>u}NpCV^GdYdPtKyDZHeW={OR=nT*^8@QT=(Mi_AOoc6^muW1gST1 z#JnGsIJiUIytx=g5zmdM%KB{Bi<>*v&3`XmhnC6Zoof8RmG#yvaUJoFx32fNaxu)l zxK5t?X?3#1Rm3afN-1&rkUE)kEp6N6Z_p#6>R-UsMm&KCnd0&CAWPiP+pmyWZr!7e_Ct2g-GpeU2kG z2b%QaEaGRyE0?;Yh|RcURO~zA8k8JTD+^qW=YFl9Q;FP^ZAEs%mbDC z(K_O#zfk|M#7)FU|HP@di z6L%4tCGC50aQnJ>Gdb+V)m`i4`F~rNR8KQvv-#%p>tu6B$oR?!*W0Qres)zxhVj|al-oLK%2DhzWuX8-j;n&n}E|0(0=mw|b zrCrRyx)D|fX98VdvWu%bs~Q)vuwV3LL18~mesRs zyxT8N%aY1RvfJmx0pg6x-y1V|L5=w=QywZa=Ce$R!xz@chsEY4j(Tw#@qxFmTa?M^ zch_$&f7a>vWA&Rnqw;(Hi&c#uep~%o(^@?l~xh+HfrKyWAhSsF`4gr z%8~}Jt^0ax{PP<1G$ZCdOWej$Zxz^OpZkc9jeo=7HJxO9=YvkgaZKhu3th&1%U0s*?RB$!1S@g+jvDjRm=c%2Ut|6q zSvNggVJE|9JgF=x9|Z1kyg5b@^R8Xuq!(wsxah@IFRpuW+l%{N9DZkAe6!ARFHU=L z-iwP~Tt>_Xma24zOA1{+O_a|nM~|$}8I9*8VzbU^FV1^$(Tl5y`S@9uw29apecRi7 z7ctN1cxjw$Z};SKMmPWYQ_rx&Q72A%aThT!#cLh+Ik|n^{LOzoF8eNVarYYYCl0qb zPA((n4;Px4KZYoAf6i0NzHa}a3$EGc?Bb`EZ}RB3Ec@)m)vQkb$cyUN@?WS;o>0H} zxfj;2W%JFG+R5ed4m-T0#{9M6`yUT9kC=DZZ#l+o#AZo@Z>*a)ar*RjpOx-AJCpl} zdGz}p4>XQ5dFTu37PmUa$&2eZc}Bl^jLUz2+TqJ!kiQ}Pna8+^n3qk7+lYD5mbi%eI*lfOw_=fnwT3vj^{BcQ%!@sBpYR-KcvDxP;Vm^YE&DRl|7rL8>%{q4xn-{wK zi22**bxBv%CFS3n-Nc8++kz6uG5M0X&`O-Xw{G6ZXKZhyk37BHw0Z9+o6jQVx!2EW zZ*aVeUh|K+l$QsKm(>Tp=1N{gY_8;W#O6vK#5NmIjyYcZ>8Qk``&h;B=e9!H^^_sYkc=f;5 zGrGZXa{8NfvUzVf>&5AB^(K39`sUtbFK*vnC$AUSKs=Fv;sMto?z+%5;&N6dYeIKF+|=fA(I-c}_J?^I*Hkf@Upo5^X! ztN#7e9btIuZ!33|e1BA4`OhNe8=RsvyiJ|Vj}*#ZR5FQ}pBj}oJu_K67ZIBe?dPNR z=;c~kMSSHsr=E8AXC}*%Mz^n<=VXcVh!(JGyVuFff3HrK2mfWne2yz|9Wh_2mbi(SuT-0uuT)E%j_ZLw`u(R4w2GJy0%daa z1$8nXlS`aLY$m7ot&{mauAJulel<3e!~55m*HZcKk22;v(-J2!nertrA5k~I=zHtp zA9~!s zr@DD_ml;LOAFNcmi22u;H!=Sj^Ae{q+1&1nh|Q(Air6e^6S29Hx4q5x5t}P{@Y(f@ znthHUHv61JY;L$|FU}%1i(f~~A1ak|-`}|&{o|+a9fP~n*j!*4n+q&s^T0BU&6{g@o_GE=Pg0|Z4|x8mIPJw{#PcR~Hw9!9v3a=2*gW{}dy^TP$>H7V0rF|L z-bN9d+h`dvUn`c$UBu=AaQJz3pUpZmHb)=DRmyHoc>7dvVu``-m^S@uN>&VB;#Eub0Xzt5L*! zy;R~nV)II18L@p_irAdyD)$+$RLjMXvAMsmW3rLo^y1YoBj(YYn8;1c zqc<_1&PrUzK66PW&f}hzFC^;b5%bMmiL2h^x)=8mn|FN6hu70=?lO}{v^QMw%$PS^ ziGxSh$!ErHN*q0^v(H(?=5Cm=xf?EW@|9nC+}+_5xWoT4Uh?Y4Tob3udZ0@#s9($E z{>}B9%YLhVz0bLazbtO~+x44w-o3s`f8dj@cleud&cyPIeCyw7H!nZ1SpRMtue{T> z51+#I;^eLEWc@(nOgw%doqY9^>ypZ?IeSODdHF5bMK4bOpq>2kZ8ouazFjT1(d;kkKJ#bL*f!*VZDjJ`EY@rO#iCJd{lh%;WL^~#JqErxa>`4Y$k{A>+CaQGr2f3 z`5VWhXUxeG2Y*-hc~zW5c?&$e-*+6Y-N7Ii-^AR!#C1$wao@T{iQ9;8``fzj636$i z6F>jIYAo{8h|Og)iQ-zN8)~Z})Qa#U(Z7ZB+KTenyQ~eqp`g zo_xIFGCuUW$6tvY3?6d$-^nH>Gfq#(-29T`=Hu_I`+WPi)~`=G#%08OTqz;L+sT_8<1S(z zy*^YvzfS&p+{Md2w-NIL%o11MT_=;SJh05ar^cMDw^1*yBIbiYnVi0&Zl2GZcRj9i z){FCAT=e4b^19FTtow|Z=U(FE2kT^BwB^xe8u8qCtSfOAG385K{7~IIK}N^LXUuD< z#8pgoV{TrrVCk`7h#?OEKe{;$Or& z=k#R$`&{)(j?F)K`rj)by{+yum2P?5JYy=AIDJQ*%+G#n{7}1jIr=nWZeHT-)1GnI z^)-*l7akuO_7N|Nf4{o?Yt$L9yncOPssC>Eb?fH&pxVTIVOHWSCi5fiuRI*|WOHWo zn;nmyF*h%9dcAs}{GsPpA17yL;-MXGj))0TCI_EhH_w*`MLuJ`JScG(lX*rZj;>!f z&&5CJpnUju18d9!z3MX#aq$^7<_%YnGdA*@+qIMB9+xpEOPq{4lNp=I)wE9L$5RDl z^c6Mc-LS-QFHWCaC-WhwOs*ro{Xf+|EOGLb`c3}R5+zQ*sdJ!NFV1^$(TmGoT=nAe zh4tu9yX2Y23wkg*Jf@%QUsPk>aP>!8FK%PG!){+vW8RweVt84NSH{<#nI=E0kq2 zWBv+diKCdz1C==L#p!>k`%I+*vW%D)?Te2~T1Wi*cwt`RE@IwB4?3RFa9Q`6N3TDV z`o1=nTXPvP&%MOqE9+#&2OW<-?!{TeL@tx_h~r>$oym;N@ee${RUiCR-TamDDE^qki=s<|=6i(0wQ#r;&%|j1GA@b|HxVy?*Qo>TB0lOLcWbbabT zgE!P~n#p0ryg3fWha0XpIgXfD$p6RJ*~fiS&-;Ham1H|>Qt4*1rjpdw)g**i6XFo- zOJ&uvCM31GOeaZg)>N{pV@=WNX0t|Q%W93^Ig~bQ(k;uH3Pr3*x?T26=&Z#0eZTM5 z>)kc)tM{Wn>if8!`+DDe-k+QK%*}Vc+ew~;ny2hPD-Sk=dipQQ`WmF9i@yx-?0XI@ z2(^nvS$eQ0)SqpY7AZ8>f}-mXXnKFbCWLF*n-VBq1*P_;z=UuP&pVL3DmiQfc7L(v zvQJhxK5^Kvl0jhL^3!^-{wvIN9_=xzeDD~ccANx?2#qrNKPZ3op5rADcE5z{`24TH zf>66yVCBJLqm2$Fp+*;2d$94~;BU5>@ae(uaVQtheu=b5N*5FA=0srdcPJN5$A*02 zsB{&fmQMDc3Uzh}Y^c;0$yn+L^-{bj6{=ET@C5VZMSFqKKWsCjQA#PHrZl||H6?-d zKVg3B53mHuUV@g*G2W{m;`V=&hv!syxav6fJaEKhNl z&w%n*$DJ~Y7wkP!MwV<1bDJDFISBnK^ zgjx`Rg$J7#!RL9e$EWmW=fP-CD0I+@GA7hO0uv7oJeYbg*$;vAtVhOtN~nPZ7KEC- zz>?7HtZL7^^jd^uE%ykiveTYI`1O#Ru zfzrVC1VCLGMA=>esN1dQ$!ha;Ks{;;jIIRKJPp)51=gNYp;2}}f=`Wp#3*{c#s-qD zkwP^WSo{P^%~Q<7pE~9Wjd`^JN^=RZCDcoZvW5))7fO9DNRC_?p*|NRF!x|bXf7cZ zolRcMtG%!x(<1LWDu_Z&USQ)X6&huZa3=9hEON$wj-F%fl^1ZC^HYn11QZ? zi231w^WTC`*^oDcdVn@i572nD=3Ow;haBX|hlWsn%GN!c3+0>-q2Fa$YYCT}hq1Kx zs72wsq15v@G0zC6^S+$iq-zMb=bi9yWS$)f^9S$68MHh!5*!6MpNC&L!e)eez3!;d zb;U}Ryk7T?u_0^-XLE6twXP$ab|I2KWE4G^hd_&Yi&*XgH^&0%u#pyZ9|qKZ7Z@FH zmD@`f6RJ{RF-5uCNLlflKU?tzr4%H{;8PzC6qpd|pdGey*i1tG;XhobC7k`LIYUhl z2y6*;ga{1zO%?r#K-oangz8fQDO8_`PNn)382ks4SD!L$!YNRc<$pq{Et2l23H9qs z=%dd;sZ|mf5o(nHzW}A0OEY6a{i2h=giyZ{C9o#cZ&V4)zX+daZT6DMdKMlmJy?0L z_F&_|ZVHq>3NLh0iaZ#5F!A8PgQ*8I59S^$JXm?K_F&_|)`Q8nQ4oEdi){9)?*Z!D zOAOSvml(L&x8E;a{JP=)$JBh{GC*196>ga8LB3^Wi@v$uOf-S?=GP7*Wp+LCeA5w! zOZ2}E7rU{7@Yp{dF$o*OwS4o0{K|9oeVA|gEqs3J8AJ1MHU60R9Cj>nIa=YSul8U` zrJC`ZB{^`f%Nuy_XEA`TR8wocVhPZkXo4b$=Za)^184{#}$NHWGTp?Ml+w7evJ4OW#++_a3wbsqKt1~k$I_8U`hCr zzrRg<4u=093vYsQ!*U#Ya4aUAbp-zLQ~M5;IpMm^d5{{uG3`k>ljk(U9vm=b`XUH{!5WzB>m3aI zHs6XZFr-r7x?te0d?$^-h)R9Ig20$?559^+U_$uVI_wz)4hWCos}2OFgyxCX%!4_h zdCavW)VJ1%&&GqDXCD3pRWd#!4<;T=J(zp2@L)x_=I;HZi)DN&)L%J~7S&Yh)4VSn z>c_I5A$hZnQK&C2kiCt<8y4Xk(*lDA=K7KWOqnTgyHTKG3Y48y?ZL)_;jb8I{@&8e zmyUeKgt~>3<7R#@lsb~-oU0_%gFa5g2-RF*@_U%;+e-uv2z4R|%n0?BCIU-B<1@Gq zKJ}F*q6`W3l_mlsLX&4qsFO>S38B8yL|{s&lS^PmsP8!um=o$NO#~K%tJmXrB(NgX z?UulXP`6tG<3FI8I=}=D2#tA4s2ej;Dl|T$`{C0RBquaoToCTh2M@((OE{MYQ-K}f zvB%@>c><#c5Xj^i6PlD#LetEQ(B?^KMo6VT`Nk2XU+> zv!habbDz<|lK&CSTyrZHRaxr_LY>+ID?;rfft?4VKf$L_mV^g#DH8K=1C+Y_N}dXJ z`4yN@sXhf}9;`eV{VxJ(bohJ}P+w{C-BCdXe+E45`50gV3&KY(!#@h_{$kBv{`OHl zAG7A;$!PW72&m?N-gBfR)Yqh}8y+Xdy3G+)m2x->wg6n+f2B$2!IknhQ(`wIFhgD+x7E*}~O?nx~v2bW?naGJF;S>AO=#UkV#j zxb~84*bzY>Fqxthp9)neFnTt8>iPTT!!6)gLa2FW!(UAp8xU&S1?Gg>c7Y9{=DB!y zJ!MRxMi*G~?JC;#bB7HWQ+OIjpTJ;i=Y|mU=AQ9Z(;~{r8c1^dhU2t6MRlmQG+w zcpWDK0ukzRA)AwSPwVrt;c4Vpu{WSrNtPgmS|x$e$Dq{5U}RZ~33UY%I3U!0oxtE^ znCrqKF!W&T!J5!S4?k{GLY`9~^7LTt!R!<#&)kEh2Wvu;XEOy#p6wJUd3J=hbf2)z z6lLbYobbT8*s02*s!)9j3{Qnmy-F-TBM)|j`jS9V2B*PXeF}^{m=J0~BzihUDX`(@ z{*;s8TYRRU!XIYXWFD-pfKpEfWXvnPlP@F_*igCjw^-H$c7!|dy=w-Z!&hw?c+XCF zF_pk}IikH?@Jhn>qB{Vu0@UNXz=+W78PfZp)GeGW)D@xbKe5ge>NFIX=cA|J zfOE;9|aav9(z#_mY#V>xbgI!GW#O_(A7p3|Js8Iqw1wjQ5J-1E-96SFQXfQ zm8YydWyF@4w#ObUE=KZ3S$Z(~3Y0n&C8gMd$#N)lYb46tgOvxP`KL?AX+bcH3Du{- z+JnLSU~ZHRq461~jxzIL<-y`;m>+!%J|!iEyMDL_J1Vqvq6|L-g@LgLEBZ3Z#)F*) zt49z>yI7(tJd2G$Jw0VjXq2s|4Avu%zS$DZ^k7M7T2yr6>hg=|gg0~M2^M2`q{1rwNh zu=HT~5yxjtc+n;JNAWozG=WMg3~W6ZUJ74E+5C2q^x~YoJ~i2!9ibLP`n`S#%2_+* zqLh?cLhW~f$-__@SbA{qh@&h#*m|&F()v?|G86}Uqa_Mu!;|d;s4c?%&HVs1PdSqc zW2=Nuwpp)P8K@f`ftjZ)2{n)?gPl=Fy;5qRUQ-nqQmGSGU_xl46PiE`pj1KCuX& z61^fcdDeuhPw6QKpF3Z=SUXMzLr%EqkU8>?r;V;eRa4+=p_dFqx#e(jj&+2` z>;&^)4xNsLOAtuA1Az!NkX)XMJ`bf{k&u2*303*>;Sx5M7mhNy08lS+%Uai73OJMh zC@@_LxO$(-flhfW(AZ_9NmL0p-DddrsGrL#?yP| z1(i4R7rCXGrDt9fZhvOayz!LTN<`P~miWvGR~*$dFV{e+V_y2GCe*b~U_-c=YaV*@ zCysgM!ODXTp|11dv-&A~>X;XpuXO^&cLC~FQ)Wj(sM|t;142Ei7npf4C)C~)Wq7v} zC?Yh0VnP!rAv8YYU%{uD9d!$+i~Y99oEZL^z9Up1_#U%=ZDI znZ@O2E|lqKQmQ;yd$4ig))$FSv;S;87;g)u+1F(rEIpXK5aye1K0yM$dHDaa=0$)y zz@&?VJps)`C|(PwH$hO(1aQ%1_!Jl%Y?Xf;9T7T0y+-|-QS|(EP)_?MK1JEkmnuIw z%xSFr5)@DDj!#KGEAfXWzxBvx^>sj#e7D>xpFL7$jH=0ha&(Xi{~wfErN52t4%F8G z>g9b&UZGyz7nuFXi%z)aX8fa!&v>6phDl8Ru!WSaB-A~vY+u8Dq14$S%5(xy2Q8Kh z!VREka?k}mqC!twb8bUn@m0{BoZul*35n?QT0Y1&j5E7b| zVL-U{mzcO>uJFOT9Jpm4W;9>*<5MJgF)s*B@+F~3srF#&!H!T@Fe!3-F`B8}AsyFE zfpUftUjpTlH)1UjbA`*caNydrdoZE7PD2^<1H#oWx?I{WFjdHHjKGpm2ZO-oDx{=a zBPm^ZBcPc_gCAKa%9L>N%jQm2J|jG198ktmPN*YUU~o5lYKz2YwbiBKON)%5NVtGE zlLdy)hSKDj5}wBcwJ0;fnS8)UU>?GJ8FzvL8^YBbiUuxt3`0?1y$#HlT!ltJNw{vM z1DA48h_Y4lzx9*~m)+Kbo%+112b1R_x|U9SR@*u$)r9N1i>0o}lW?3X1X3b2(OWg| zx2RLtPf6jDev6Xrkb+eo>4etYgXtMgpxlGmS)S5^-5;PlbbP7w zk)#yf@4(~%3#A~b2b;e^xq`k$sc_T(;vZ4uC#+JUcZ8}GnEVq;g}V&19m@#UM@U{^ z^j!S0@_Javd0ch?;LSVtnwb+GasWC`0u5dYg@MV-99R-+$BB9U0VrqQ@ouT7oPcK^ z1k@dijL+&AK(m51ggQH9Rm?s_`rxHbeaPP9;~K73>y!|3$0I4W*)4jK*_V60>wN$-SL@tF!NyaNtmB` z9X`cp`WgJOE_dMg*M2bB#Tk{_o04boS(uHV(KA>0dRj=Jl1gJ6x^^z0VE4gJa|w*i`S?E&GsoAHklDETq|FwLyi0-BU+h5eKog?v1}3?6pOV-Kbt3^rPG*%Fsi zpsZjGp+1m+WsUHL2QQoK_m*&*=K@Y2jZcN=uf6uE%9T4pDa)@a^~6C6qVU9p*FV*K z?#(w(!tin1BH2+#Oy%HRuM?$IUZF;pwkv!rLP`c|i;U0nc$#H=u9&#|sezV%ebrN; zHdE@U(Y2WdYLRywIvFe3B0V=0rNZ$SpqWxSg%d2YeC0&pqCfO1ukd{O#$ezd3x3nv zM5%Juz0gb(XeIkddQ+8i?nfXgT}z+S`*|u{($7=jvTb_Zq43Uro(fm~x|gTI`}%n* zT-Q%2-4+4XGSGITA}gG}6aG<3r|=!LkSZnHK{1EsQV@j`GzVn!4(N~hgnxWtSGW;n zv@`zLc}1@`70$Wdf#bX1A_L5r-?Qj?fzlmn{@5RS(=cRIo!W9gE+W)X2cLvG<1pq4 z?K~pXukaY3I_8bJj(G!hxiCKm1S$!&$g{P8h8-O9vo|@)xjZULGc~0>`bSuW+i-&>%3>T7LHA2C z;}mMY%L1ry*ZvZua6!`>^9uDcuL-nZZSR1h%A05PW?Z-*QZmsK!VfTCnQ;owe<>^^ z(11#9ktE+xp-|3H6sk{|2nsd2_*8gw|8k1L+xsI~;bzQ2@>IC$gT2|I&?Mh7Pfbap zD^#V-IE5xpg-4q`1AQL+ie8mEuOI~#>QiQ%LiH)Iq*CjNx%qTZlb04%RBB4{%7~h9 z`s;c#PT|B09k}e)-b7I4d=IYm;A#&}zs>PE(}Uw4oZde}(UfL-@aWHCGlc=>l`c9K z9X9ut-jq?eEstO_7!+>W0TwtO(fo-EdZSL2$DMY)tTsley(uZFa@GUAsjYC)cY3S0 z!j&KD4Y1$@{4w(bmr5X+aS7q3Z}wJig%>{DGgo-?i+d}BLT$U`sZgV1&%i);acP(F zIrsqrteo`{NolL$|Hr}~0-8OTLbC^psGM^Tc0saS1UJHb{%*ZIBSPIkqMoYkZ_H{! zJ#86&<79Y9y9qv5Z(KUE#4%3cCJ)a3o1r)Rk6XM5Wnk=7f5~;vd7McC5VvDLr^IKE=HFCH`3Sek_#&v%3K| z^kL59x>=|dF28Wz$P&v%L8Vzk6q>=H&pzWu z6qpn0&dNaDRSGPr)XlSj`|o@CsD}fA4V7E+7L0*QKh;yVUi9wiph+p)4!-mYL=q_X zU_oe-SGdjEbTavpN*&4KGuj)0HtpG)2o>9GeAXTe_k+24WF?Fp7&jmd;bQgqo80>^xZWYNoDB zl4tx;r~j0yGC76KDOy=5RUCDd=h2n;`S zxin87u@D#$Y8MNP33dM|FeO~MfA4f4BQ$x|gjzZ=PZnP;(GAQ#3#d0iL|GAD#AQQZ zM`-d?Xj&A00X~b1J`bUKHLIgUN&zgxcBRugr=S>dU!4**I)RxQp*-l>*#j%U< z`HbOTV>zMexRP+ySv_Ut!N!BF2RjdjJ0pMz6nQZA;J|~a2XhY=9;`fAd$9FjFvDq4 z=)u^71>tJ`{M^h@A1U1M$~n@30xK%@<cn_4C5-zxLTxuX0pXsNpPk{}`rRMp< zQJ~~(tK579qt5_po&w9yI?C)EM;ToJxa!^blq0OdyA}dUJ(CNqQu0)&N`Wnv)971Z z@Lw=DZI1|5xw*9HA}ICM7GfR|>I+c?W`x>yf#Ic2putkWL)rflC?zz}gUg^)pQ0Ri zFeTJ&j3_e~ei=SzGN35C8^1AZZ4l@PLFI1()GEmWSn}?#zU@t#sZe(pa=EXf^1R>R z;Z+0miB^HFr&MT^!Ow7&(D+nnlp&S+9v%s#P@j?&Sl~JNZAF$_S0mj&RLAz0w5_!Cd=Y z%oS?C3rswvLZcjbN`*$5QK@4I$rI{W5*V&Wo@Ovagk~@(G=rg}(!kn-(H{}WjL+(S z0Zlz?4|X0*JI6dHG#%G?%H&a)n~qBfO+9lDmL9ALO_4i7-6u=sTTVYyy7>Q)l7Yz- zC=;Qbfw6wZQG3gnm&<4!;mN$lCNSLv$`iT32#jU|&Zh-_7W0i3%1Rr(32-52vn)aJ zzXLw}4{UTrS-u%?-TQm{Ie~7c(CE^TRj;;^7~#V9cH??^~HTa}Sn$sKtzs?3)O*X5Q+_V@FQ-sx$GA;kmuQ0JxY=pG0TdGIm=~W4wT}emRN4_jsHf^kp3wAra3!K^N}>!2H6?*Dp{8V@ zrX(<-(tJIn{RRS=wXWigUNe@W??P!>lo0AyVUcnaU@DzG4&|DmOmeH2^^pXTDj zfY6Mk^g1XvUWHGYuodrTYw56oB-DZ!sFykgHdJbN2y8v`gpa@IP!y#?6G)*6l+)bo z(iQ6Xl;^DCPhKz8(IQKr^y#2!drqZkQOD=i4m|_D#b?Gpw2K7}&V)j{LtsIu-660c zT+H{_$vJFGxS9{l2rSQnPaR+av$L)Hm6}=Z#ME#Dl?2Q0n-EIiXpXB0{q*ObE?l zm3lBE)OjR@ zlol0y2F}3RgDs(6JrMKGgT>F#N1Bo-D?&Aw@fq9>rQT2zW$3|@qfPHgiL&)z_$&A{ z%IZ0{$O`s%j{WhW{aCjR;AVXoZ4bC)0X}8MB|GDfXIJq3AH(d&QbP49uqM=(mkMkN zHITq~27JD%@3Y>;fi0na4|?BG@(T5P&;o;*FxMOXvN9Be+9H927g%LGq+@XesNVq> zpB3S%?eLGHY+r~!bfK2+2=)Lp?`NoA1ZckdpU(m`c?SCc>aP+@o*ALOlGMO8&xeJ9 zD|YR{bYJ|T>%1uQ{Q%AP4GTg&ph%0t7)reXBru%q)I{1}cYOfEipZp;h9bN|%~6zvFey~8Nc6&mw!XDGEGq8t#Kw&#Se zW|c%4L@+nXh!4J-Krx}ov+|U+r)>BvzVX=-8lTA*ek{Fc4!hkYfO?2T@|QX=Uh0^K zUjj4}HYPMFC4{E(3iWQaL{F(STeyr+e>6dq3hlmb8B)^Q;-ZWRjn9P8n5QMoC;DIR z%L(Jy?3M_F(71Xr-6uj{tRUUO7A!VNqAOe`dNZ>oJ^O?(glPkCeP*0Xoc@LI%K&hv| zqHH}F-svdo3lP=3CZ#3R7D+SnFF>jNE-?KfpnmU6U`A-nOTy*9J6GntC@W7{6VAP$ zw=y)IvL!TM(N%cBc9%^CQfR)n8(fOy^@t!Tg@iMwqgnz>!mBt-1P;Cmb3Kof$`^#j zXUeWMFe99~q}R;WQ-)U}(4wO+oovy7aQ)+eGV0o^pxkhKukGnK0L@p86yDYULaRdk zX16p`p?-yY`e?!`)Ni1RGV=l@D-hibhVEN{=9>#)1*qTG7M}|BtJxA=p?-;5lrhcq zYyJWgLKCPaG$|=OXi=}o^)*PzbX-HIOQi(r2p4|i_Q^g9u64{qLSr6#N`=Pfz%$Q0 zbA`sd@XSj>qpUoiwP)UX=ACCAd=CXNZI1{|^qA08KJm;`&ph+YbI-i=VCBKugN+AU z4|X05u5$_!dNA@}?7_r?0}rMi%sp6mu=HT%!N!BF2Rjc2tGp_CFd?+VhR_VK)HBaL zSa`7XVCBKugN+AU4|X05uJ;P!!N`NL2NMqtJeYbg_h8|{(u1`J8xOV~>^vBJA5}8_ z9uk@n5)qnpDe>UIgQ*8I59S^$JXm_L@?h=3hS0RVB{XgCJo9k1Gr%Gb#vV*OI3P4B zrGzG>%rh@M^U^b~JoDC5Dl{ntKXBR}5*lShXp)aT^UPB!G(HQ@ye2ft#`D>F=3(tj zgow~4PiQ8>z%x%h^UO0ZJoC~suRQb4GY@V+i%jw%p-Da=G^HDO=Ba01dP;@HXYHAH zghm7&UPC@J&zL@T??hcca2V0JHnM8xNvl~ zhU=dSXa2l*QB>jhEq6^uSGe{j2Ts2W#l~qM11-AQQy#Z$GJ5zu3 zq{{hJ%F{jy^%9L-TT}R*iC)_kPT#SYr^2}(c9bi3aFpvjIN{~F==qNMp2s?YHtpgl z4}Q2eLNw3WUZ6S0J4OD=(RWVvrkYRplArCt2@h`C*~xR0*UU|x`N}(cqwdL+ycSKg zPQS19M#zTWIm(ItNY+3%c=cT3Dc5?*|HVsbnU~Tc&*!cmar$VE7ihj$kd2k_oC1A;0CXmi#+9)A8{6zC0_IiFZq*R;Iw^%7if1+ zxx`bh_TYFwrR0Y=A}l%|pK?ISZp0rOE}b{If+^g%%i&LjJAC}8r@|S@Tb~M#JbKO~ zEN?;}J;KTeiEakegQ?sz?QXS7z}p;U_9Ls57S%rkG?&d=LX9rU=r>TBXAfe+hhN*< z9wdZ^vRY!E5}G?=8KDW36CUuqUX=<$vtKF+O(2C2CcTtuFOb4jyeBDnHdKCKY41(T ztrxu`G=ak3qDu34s}Q9lG|h|&wMEj!3h%tB*Y*LGCQwQ^&Ks2yDDwj4g!^~Bp;!=V zbTKapO`yv2*?KTp=M1ot&;+UoO~)xT(HknS;oV^L5#e91!(Bmvtrtk)#E!kWsnB#s z=b4AULyJtF3Qe97l_pPxCeN5k6Fni^|5?3-Wk6_3mlB$k6q=NBD!2M}uS$jIQ{h>` zk&{c1LX&6dnb(9SdPAtU+R;aZ#%D*k#c$?LMh{w4-n2a=G=U;Q<1_Zm6&~=&5tD%u zPdV@cWrX+5e9xr0LK8jre3qWiitrph0U=eY360N2;Tw8YY6(r1Izm&W;9h5LhJ?pH zh<}vm5utfezO{m}f zKerDL>~Js@*iw1!Vz?2QZ?HbM8ipHd3H6z%b4EVXjaDgD$_Uqg9{(t?_`6lgDR4=+ zxQnGl0xQCg@aZ{$t!ExQ0iOr(n2ghE!etNld`5)!5sOVWCCM|Nj$YJy0^o|`0m)+MJp9-HivUk*0xaS9Z`?`dI z9{Ybd1(s1aAYA)OWFfF1)D}td9pU(HZq7{%^{Dy^=bq`nYu5DE5LM3m zTCeR2AAV`C?Fwi7thY5%IB{IR?FXYJx-FFCgMSD7%k!`ZNHfE?0GjRyJ`QLeW(x_; z_{<4^_u2k5B;0W69;0!9p;!=(^HC)kAqtoAQ6&Rs?9hL#$cx?)uJ{Y4p_qrKAbFFg z!g+t|DPt;iWf1d(@QJ^!l`a;T66$;xm=Ui3d(UT1_}?$+J#(V)jQ{H?3o5_QRZ)B@ zJdrDez>>-vzTYcydj^`R;}hqwX9BL^^VDLV5FWG$|0u8_Jnv0C*b-j!J_oLt(}NwA zJ8&5mpYf-mSiMW{`cguud5W?-8%h_xX@}lHD*6nRi{acg zU$oO+lk=z|G|Itkjxr-O$wxnO@=Sm1z;KNN8xN*Gag?P82S0U`gSCL>^1i|a*EExD zPpMpS(6>i@hE-AFmS69Ud4x>(_I-t)n*@lwhNH-5YqsBDn@TE2^0%xgkZ z`RoBGpSTa7qRa``@A-?#W-459O>eOZ9)j7byk|am7=M_#sc`zXy=_eTh@-4LSbMPX zVC%tPy%Q+(;NXvrGWB5P!P4SdOgQc0-h3|z zO~=)qc{2sdK`PsTJk6+Uw#2aB`7^!cx0?cG8%9$5IDKI6}g<4=nsAnhwb3#2C z5g7a%d>+JA9IH3sB4!~lCtUMKM8^qE2=ldD<5R8y2Cu~*W*)_yy#@{l%~@pd-!Ru- z1H`8EI>7mR_GdBSIq&Piig5N`Jy;X!?*_^&E^mg<*)N1r0#yo++*_u$z?yI+qZ_#9 zT(}W9xCMWhoqtAX+TJ}5r8W~O{T*=LQN84o&G5(iD|-86h59x^F;A&nK;HtZZD77` zw_Y(uzUlPd#!R94E?bf!x)xcgq)>}&pcWbRVy zB2=aL9C%8F=CGT2<{^*Pnv(d832h)k<1_WlGta#6%uCO_^2{60y!FgG&pcX=dYa^8 zLeuty(6l}C%)=LBub{Kz8n9y{(bLl^&e%;J61jZ0-5<;DiUqJ-A_-=hK4| z9vt`JhG%;|JviaPaSv|T%Jb>L2@j5YaKp1apB|j>;J61jZ0Y&*;DiUqJ-FeSo=*=> zcyQc<8@BL#dT^o-+bLsy_tBUy_p%dVbetV)o(|gIDx%W-)RCH-pE^=#ezsNN%KlHm zDqQBl)gD~yLG$yn>T?5?vfWZRr~i{o3g>%p!h?%EXnwd#ed-Ta;n=~_ZQAqQqlFtM zVyc|e|2Zm!=GUwgPI$^i9$ezVWgcAVLGue)8hx#&+~C1Y9yC9&r9RCMY$-H9u%&P| ze|5{$bB+g>d=BsDkVB-Jo8KB%xc2JpC%Yrt2eZSTS`zB9Lwpth&mN7EoKO#ZvdK?hVrQ|yhESCfD1VvtDVL6GLRHGwX{(o8p8}%;0ac0QUuk_} zr}`?Z6!YL9$7e=pe3t+G7aR@HunM*UZBeJS$pPmMRA_vbo_S4Zl#S=J^~}S~y=D>`pE03n`@mDCp3lrP zFFfA4p$p>3FgSNfFX?yTPM;Q_tpAn%M-mzys@XS-sJoC)+^lmx6>)uB0 zR+oe(dUXPnvyS_fSjd*6CNvKZC|q$9ER1qZ@aswQ!AGGmfl|VIuIOE4R=9vKd=j4u zpSY)YFN(U+Y*E^UAANLdih{$vl99;^uUby#9vdoVbg_1t>j$s#9&YAz`aJeYk3 z=9_-ryHS-BPX7gGuJ(N&+)N?bgy^P9?FPVKaFWThaKZmNFd@_# zC(5pKl<}j0dZS8|384uzAk??Hin1UyL$USDgFhqCU*3mLF%Jo^I2^-9U_|(qqk77m z@QHW#;DE;=eZ#i&QAT*i&b{TgAiQ(X8=n=SIrI#U$Fa@8V1WZG4;CMR(rjZ&57r)R zJlJ}$^I&j-6Fu@^?7_r?0}rMi%sg0lu=HT%!PcPx| zxd#gmmL9A<*m$t@VCTW$qfV6~55^u$JUH-R>cQNDg$GLyR)pVP^6trF#~?$C^c`-p zGNgp&MR~agOG2}!RcOqUl?Y^(%9`-zclMUG=37vj19Vtloq(n1z8Ct$>BVf=XRfajkNSPl4?1xAG0c7cfpb3%PDu_zU4iv*Tbp2LUh1=gO=hS0q5 zyd}JWJ8Chneu<>l^0Y;+&nukxS?^q?_!X48A(tYDzX#NF8R;X1%c9#SOPBuv%IV($ zl#BMo{eU`Xrw#RE3eWpAb}Zsk;ig}}LX^P+)_izkI-J@M0&ez?{Uo};giv?X0&7Bz zE-5vH=ik?ByTYUI2b7e`hY)Dynx0bO64uiw=k)7Y(|l!L8H{1?rRUmG;J4Xi!bc(5frd26^4pHYZE6rx3h8c2qB>%ndt zo02Gl=Q=Rl)`5`+8xOV~>^vB3=L8Bp7tl>TEvFH#Br;iRO$rSkI zQJ~C&EumifMaL29wO@hBVFA?xl ze1n(#%zjD*yF_zQ{kMA4xIQJpo}_I&i|65T=uvF@4D83GymR$rI%-# zLZQh^A7z9a-`O+I3H9fw(3^y((6_+KgSBU_(3m%B-v13sg(jue^QqAI?9^vJ&){e@ z&nROL4m_B8F!x~L!P0}Z2OAG|9t_^^v?%gmOlW#jp(#k>nWvt)LSvqJN`*$5Q)z}` zL8uF$46x{fXr?AFYu(@&K)XGd0%daLAA(YM7cybfk6MWJlTdvMOfo2!J$tS!)G#NU zKdlFI!aFBmAyTFd{>@?AEAE+uK@R1C%X=vmgfpId`J}QTeB$^|PQv&M zm|w)-h>+wZ>T*&sn8R*zN+W#9`vU01vwY zDaqp{>BWExd5Dx#jN($jCoaS%#{5$Jp?M0-2+iy$zXYWYT8XZ3$)l%BJq4y;hH}|I z0A+TRggOlc)`VZ>QY5e;)OAT{2r7#xg=0YID@OWnAe2Hyz$KA>)>~V52hY$xFTpuaxl&RW_=2*2~~;nxUXXj>8T~w zy5)d+yF_42sOADw4^|$`uXF+xgeFi$XacoY!F&aX73ChRJQ#lyzE-gY zXy!h@m4#2EOBWBu9atRzsJ$slg|j||e-xPK_`^J%(wqgj>v270I|WKg-4rN3+fO?_ zJ3^CE_gN=U_<2Cx>`9>9gJA)sDM;eM=6oopFSt)iC<83G0C0R>4@QKu`^x%a8%WHn zO8~V+0^3WiQVJ3^fLHt!pQuvQN-A>>Lv#a|y!Q9-c$2@g8y!O1?# z2+anv;5=V+F#1R?GRG(54}Dg1*P)ZK>=X;7Ma|WK%Rh$C=Z%yd;hXNqrDK8dN+=90 z2sMx>TS8ra1xDY3xh{Zmh#U}_F`xXvD&_8KN~p@sMtN2@LAmt8`zNbZ6Y7kU@!1is zds%O>3U7w_vOcT`HISHxw?KL0A5aj1?X7^??*a$60Z#i@FQuH&m=!r5G#r90}~q14Jt^z^lW^SF(bHKZV1 zz|;h$36!%+d~QCfXGN$!1$Kl>Z|Et5qwt5WHnPzTJs7{wDkb^EgDIhod1+DO!PbNE zsR*PinA9^~2xyK71H#o0{a%&}>5i08yTia=zZU&2F!PiJ;Tz7`chYC+!QgbHq(=mF z+?h^vBL z!D(jX!Nh~X7oCEHQ=lXtc`zX~1sQlS_sk0qR-SpxbJrQg?_|oz2q_758e-I4WLqRF zSWam2RH%bNl#OTJdgcm^d2q4Q9iayk4-PyST?(Ju@;U?N5us^O;lYaV-Xq~gmfzY_ zDl{{$^_1PyL1P{)^$J2bkF!}?6cU3IYdqL`=A8%g z%g}andQ}jblyV+f^>`!)(}Hl_Ik?~^u=HT`6$COvvE<&%Z1x&Lvx%y?_cF?k&?w_; z5J;7>F-r-Jvbz?_`@f4%IZU+N7MNy+KZL?GGxA_^6O=j_P^I7jSrKNRf=?Ms9se*X zrJsO8lYh?W5LuoIxb$`SlomCF)|?j^&9%zhg9V|vfLVL6@nGk{@ME~dX|8|99vpZu zBV2!P?~&<_&^&P+os2-{iED-CIqKL`Dm2Q3N*$k=?;l4X10xS6gr=SY4`v=LJXm?K zAv8s9J!No;(;Xq9x$+!&aIj?iQ4Q?NxKhG5Z*{4RXsJ@kx2Kt*7@jgi%$II`n7xG$|=G$+uLRJd*-} zHvG0XVKWaFgl1hT3C)zL2utId7dbS2+I4p3mTWP;Ll%N`?tcMuQ=}QlRg!0zqI!=CDC>8X_NyGR;!@= z&c>s9J_$|qa5a>AjYUdV`~dKnGxn0^8hGm`9C*q(Jy?0>3XQo!W8Qe?3XQo!W8Tty z!_6&Bk4qq)gbq4BBE_*7_o1`VQ~SR#-t)S(9>LJfo^-Gj|(&zC~n zzW|@2YzepIr@)SX=sGVjSO_x%lPOSkR)Z-}%ySPGUxiOyKSddS&4B|CRvs*`aLkjh zJ8Z zH(YbZqS;UypDCe<9{&PLHGlrdJS9{mPHf*FN%G@g`kE|j7$F`EJ_w~Q{^(7@Q)l$d zBTpH7%EVI+o(`Hospm8E%yUm!c*@dKR!;{_L2A!uV^Owv=2S2-{uoZVL@gqtqznU|h&@R40dzJv9*ph^;`^k6;#<)Xjzlr`a@JM>_u@bf24 zwx~E6<}(-IQv%hWz#sZtx(u6O3E(lyUnHshZrJf-3UzPuhY`#kh0=6KPH4KLAT-?( z{u$<`ixWbfT#{$z!F1YglHbxdeq5R7eo1JP$t2k0L2t{9&9Q$u#V!)E{FN80-M^>HE!-f(VQV^{hu=LukG^ z+s=f!seJJQ2PTmNI}g_TK&k5|Qrg!s561zuAkyy@p-Cw?z?!4-9;^tby#NIfW$;p% z>oqHZG2ycR!s)8O!4#$370L)TB~g~IgwJ^&#lj+2p0nA2x_*kXCe+FcYzVdO0$UGu z9?TL1(jv<&4iB~vDNTW*EM5oY5yxYIiL!jXHJ6mCHv;MjxR}>(vP$@TGoTh(`n@L9 zB4a3e%GQJFTj0}-`I2z@HYZPx`ReUZYLO*S@D9M;cj;Y`$leKf#Ia~Qk|#9HtO&I? z(RRW^SK+8FuqB*+Ce~zu@nHzG>EH1wDJ6tvZkB|mbPb^?UF#`34Io)T*E z0&_w=lq1h0V7`Q_j=*>>pf11gNvN{}K3#Yu%yrOWz7y(1kh7k_QBWG6N$Qv&H$7aRaDMhj8P{(YeF3%0z1M@??Or_-TR$9 z6G9Cn<_b+p11hJLy*yJjXY%L{!Wpak$rEakMOhQBKNU(0Z-t-g!Sn-2e%>2;i>ktl zj_tvU%2})ds-&>rM-Aa@(?=gfpbh_lMODn>V*uxVs26BJxNcexW`x@=eTQrl#JnQZ z$tAEQ)X60<_z(gaW$3|}P?rlaPYBIMHz(AU0VzGH?B&@Jn&{E7NXg_G6B=dW!IaSC znGu>iYeF5~G8h^{9o_<~4} zb`MsldL#PW2%ojkZM+AY{M*#Jm%mQ;leJ8WP(t|ajseI$XmT)eIIeeag z=;nCT5$ake%J3>E%|3Z>6QCAEx+C>q?!n^e;DK}Zo;-1g-+&Wut*0#1wFlETTBV%W zrtbsP3&N6TmjY@t1x80Zuprdv@=R3cDbx4c=%TDX?D&k2b71=s2WBT&C~Yr1m`qqD zmR}EcQ=r^c4?k+n1(qIcJXmEg*TH}#eG0@I4o|d7X;CxA379_&k{b z1?GgBlE7jLl<4_Fn7@N{l{`B_?RRNWbUKteY>@mXy%sHUlwl4y`*?i*e7Msc8=URH z<}-k+PQ~Zm!$@PSFayk77GF~Pk#iTOE2ib;&HD^ ze|KQ*!NC)bGXE!__PdPaickj_X2%vU9DP3dm;u^OxCc{1+jp``F^_fyT=G183hbT^ z?s{YIZeY9{%+8B?=Ed&#!{pf!ew)4#i11dr5g5D><~y*t0<#wZ-bo9Xf1FYIj{>7p z0T0!G92RFR`xKz5XP#RqRVqAKda(9jGX+XYtq0@9h;FKsoQC_^cfF~1BQ+&l)PMU^ zMYv?wJx4JDSrrxT@ane;MD$DGQ{N6TzQwR03Gcry+!NoZ66N6O;M#ullFAiFy>}FR zc>Qm*SP{-mdobc1dOa)u(ny&T>T?3m=|g=^z$m9bjyv_(gVB8Y4!CIl*^zlm`10vk zSj4BoMX$gU1>#fT65jn6p9(iTuje!RGD>$M4;Ob07tpbiaNYL38|W3`^s_K=cO4Zu z_zuj^_|aVH4p~$q560I*x%O9>T(VFrJnU;d*xg}!QwD8(C!oHmN#KC+m_6{yM}aw^ z4hD>Q!b4uvQ+897Na^Ryv*@KXAUuMvGD0B2&G8#@ za|7?>h!z+=0Oh*XsJy^@8m>)mn1vPzEC|P@_d2e8A(Unswl4x)yLWFMb%f{bj(-%N z*`D}g_H%naD;Mqs<)R1^cGTFhickZ|jg|BzP_DikMHbk-+y)w5j~W{sXrUB&@Jc|_ zqWTcPNB;-alA+iT>aTknxNs%v3Ha|Y*Y#5ZH44Add-9oxaTrd z{)?j`t54n2{-F=gTZWWQ>PKI>H+&kn`YX?rg5ZW4lfUM|g9W~!?{m>*h<@8}$~_r< z>FvFTTQsGWtBxER>gI$#&%b@&$;xMhrsMKMQMwiED=BhG_}KW|NuLTI`%PHmpE5ZYK$}X_>l+nPpU7`o? za9}tEiqFV{i3d}{`M2S~ckb}M_?SYi(yOHHo_XQH^68+tB2jzFmhiuK#3CRq>ZT~A zAmKZmfA`ji+Fiw}FMa{1|w`Mhyl*)!%_RF2PiyF1WyoVMux_q_J0(a&Du zz^|OrJ3vQ=IUN^!a4-c*$0;-^rJgeLVBx{igWVJ;r3(&6@@5GNJ(v>eJd)%yLc4}| zu=HT%!Ito@{_ zgHj(Koi*A>6olF$93qdm(FG=iCQ#wQU;)f^=P!Yh3BXy$;!_r@=+pQ^&t>i&?L)G& z0X3!FM@3FP3#iehkAiam^(E2r9$zUeG%}yfAkJ#4dJ3=v4KQN9?bs>=6WV2 zgCV>Ka3KTkAw!XH*#pDj&TXdoY0! z;a67nU`jai1HEIh!aYyy9g7vt_)hOwtZ?00T;Y*5MBznI@35=z$VI(%N#Sv)CZiOw z6HvI*KYNErg`3{$S>C%K_(qA2+P_AMF)e!UKK-^A)3}Mpr_4(Qc^He~zxtD_r|x2Tq)TX38c? zmCJYn{)Umyf<9F#DJj%I25KOI&5w|hUZ%jH{V||9hiwV332@m@l-;kO)TI&^?SBoZ z*KM#S6Y6pyFecRNHUe|P6_?<0ih+N*tOv_`5NQ1;kdm}0{TtvtbR#g>3J2zE*j#}j z;kwg$gCU#-fWP?3Rk4PF|Tl4WaH>MA;H9nATH<&vDvb5}Iaqgr=DaO*0jmW-2tz3`0a;_bhx$o)Mw$6$Ms= z&+m6fwGGWHtTr<08bbXsRt!bLP3w9WbK>X1T)(6s$^qg0Phu>C@aE8 zcjz5qv+bc=z#A-35*nZ3^Pn^^Av~I2rV;bpQ-(V@<_)3gj(A5$S$i6a~I5jPkZN% z(DYF~1E!7JcXpCvZ%_BtC)4$O|& zQ!2duhMuyaQr8gi8NL#M42(QDAk>SZvIHqS{uCS$#Aiz7N&ok*$viW{=|919)S}D@ zbxjsn5E`E~p(%*M+ke<=X6q>xp7Gt@b;aOSX#4VGKRKCaNO*Gp#|T8((K}b(3}E43BP~Bq_Xq^DSXG)7fmWFDoy2U zLi0;Wji>B9n7$fqH$L0h4(vP_yw*{Mgl5=8o-!sh!zS^Rod=`Di5`0}@nA=&kABHW z4i1J-12aN1;|jtP`@d#Y5^6nh&?h{jf6>13eAa~Ku&dBsW4Qo%F8B?e>XbkUq50}o z>cPx|xd#gmmL9A;SbMPbVCTW$3uvZkQRuJeU)jFSse(p5K0x?ohbw z-rng|LG$THVGR*wJtdHw4k$doe-5i~-fw#+p$gye>^F|w;e1o!x?NF18QuzS81ydl zD%|F*-hN);*j^6&%9W1!uFve9?W+0Fn>o-7T2*ejZ|`ik*#`SLokw3AUF8UPSHSE9 zVh`4YYA$VWJQ(keKzi9n?l885dXYq6wg;3N{qj*tHKAT#dhV$D8E;`OVR0xVC*d}$@sIh)XZ%b2p-*7S6^Q}iS1-ekT3|)Et^t&>l-%W*r-Zv3 zb3!$j)4=F%C(rO#)~6&N5#C3i0%Jnc%#=_ALAf42S3HXA403C@`75CIk=$}k9s|_M z%j1qMq2B11Tf@OdC=HAVFXAHsxQR@tfdsaMHqa*cJoI%qZIL|7f7z5|QyK=i%%{Uf znwb)+Pf^BWP#Rbe8uQ>8)~AfRl2C8wJ!6;A_$1VcAj)(zYc45OgeH3DDU;2eJZnOe zXSju<%n6OMnWB_D>t|YXz%4D5^)q~yg;LLCD?k&dAk=2c59Vgic9e|=vuTbp*xG@y z2M5!kJnuIcHlrVrA1eqCx*fwuV693n1_JZ#V7}X0C}nE5gwwu-f0VX&ggTN17TZH{ z-}1haaM^cpI`Ga>N*$rzaS)j82s2fR&zf*4Zz9VyjCO)jpLPg z1V+y%WZSWV%>+D%&%g>y31>al^H~#WbV(_EflX<+cn`086RzabUgEQipwtl}=J5-e z5<702k$J9A7i@uhK&gEs%E5~PwR8eg50-?Qyc9Xu3+4*Zc0#QuQkrG+6lJ5ZU(aqI zC`~=XeF059GeQ%+_Fym$b5qa3et=p}S#9bVQ0J!1;`SgwbC~En7`)n1h91la&*eaq z=n8-QGPn_#drE~yS$ax^Mp=1Eg+|%E-L^;$<=p`Ak=^kry{Yi1*YsfV4*c;JcD0x* zT=y3IBlZmM#2;E@z{3DFkR0>}gc=Atfy13Z5upiG5NaSPa(N8Qr*nCedr}JDG9Uja zF!+#F$_P=YN`dKzp}c1|tcuvJ5zg5W&y>D*G&eKCnS9XHC@1)!={H9EI#tdY!*ivJ_hsSxW7X)3HA0Us&q1x3MG1U3ZU-m-Y}$N6``hd_b7RV>(9q&i*#JZ zSAgBKdGFSS!Z~O5&UzF+!PF#rM{_+#xPA1zVtE=;(sz#SB&8$Nw|@Pg4=?&SEWX}{ zn!G&upgtEbf>NfT!k68JF)s%xg_}-=Ql_@T4gIHN6>8~>xfaAgEr@}-b(eyu&n>vG zN0k;L745julaOP<>44hr0wY4bS1uE_Ak-p{-d;G?dNBSZe6Hc)LMB2=xQ>e}3PL!W z3!%V*#nsYDpqfyhiU&Lsfezx>?}qkc@maP-cqo)m+b*ynG%X4i!~C8H(3{(h#!_(( zpx(9IS_T;5MW4Yx3JlM+N@-C{s7iqep{~gW>YyFQ89p>Zr4CwwIpOM+2q@+Sp>8z= z2IoOB;}6)F35*GKSBdC^`pk*I{6Ar?OC^>yLbC*g=R;|lSzG|9kF1E#Cm~BHu=+13 zwLA746?t$mpmxU_WYk>>c+f@o6c{hH<~TDY)OuntEQ3;KoSa%FgiE$XzXN^?O0B2t z00-AtD35KlQ=lxW@r_WfJ)?KOIPqY*2}-@#CLUVsJJ!EtQ3IY>o@J7J#J8&6I%-f>@&3&%u{eUKVxaBPIX<$S+Yo~k^ zkN0H=jn9P8+fc)=uC#K4EBbZxd{>ynv@jIzIt?y&!HGm`KrHSL`ySc&s^c_f7iRI6#gfo+dzcN z_W#smpoGvAdEl9+9?U%R+*1}FEIl~jlLU5vc`)Hat7o6kd-h;JXxiR*u;h0z_MhE* zAfX~O=A8!vu1AZ*p1DF}9#Uyw!KWxpGfNM~|G%&MkNc%8>jXY0R2I?W*OJmu8bg;h z+J{k8MC>^Ipn{W!Q7}vtClr5lwx=mI)Z@}r8g8sO{z?!#JJ}KndK$zcMR8o#s4yI% zG?#tRD30J>-tbt9o{i%=?ifGGm_5N5BLAzegf&M%w9%*x2My0roF;ZVg5ay9^Y2m zN1+l(T^baQ3MYlDM~GqO3JZlLF#2g1x|PBj3+twzNcQ3eNF!?R4|m`IV;inRt&k}gogOY=4qas`2O*qe6p%M5K zxFR4t=I&&Y3w-?$7g2UP8x$_v(AwFi#Qt$sWg@|IqQi_a%>l1YUSmg87vmNmuCwFw(7hV5A$i zDl#x4edcfAF4=r`z=$-QKF(eG{Gkiw9f9%M!xtS2-O-O6dFi2Jb7)#L#bqc3j zJTg9B*?orU(~S0QOZFMZsD9LX>Iz`Y5@C$Ua6n}2hKBQPT*y9J=6~%Nowu=9f8$8U zrS7vF=^O4Vj`55x;okrBd^;N&uKt%tUVeV^{d)nV^uX^+(+5Px^C8~m|MoTsbBT9( zPudo*rUsfbsBi+(acNe#`hGFYLSd;edxEF$IVC-v0XI`D6;=vc zg`L7);ixb>(fdhVS}DvG4o~s)jdVoSNdo7m3M@|+I6cjg&hLSAc~GC?k+c*Wg{{I~ z;h=C-I4R7YF1oZ*m@6z5RzO;`wZdMd4+=+x-H(cyUx0L$S?v;$fpqE_5J}sp_(@NH z`Ik47i@j3?b_xfDv%>7BM4P$7LSdz_RoE%)6^;rgg|os8@3G>kQ>{sf;_!|Z4LKj>_@0`kcec<}{iY@Oo@;QO)Pdz&xuHfhbT6gI&4X2jB4;FC zst}O6)C8u5I^cb?f9GR`df@wRy=AM=0Hha@1=5SiMnpaVZz=Q60}p&9DKr7;udU5M z`fF?12Yi_H#{_dAMHWCBd;bwnkJq5t&4<8v4cfccvmY3*L9=h}zJuv&&?dAQZ}GMC z!1!}%h6^I&%S6KXa+Wauju_!}Px8;3_VsR2 z6B1t{TcLg%+So^6+%+9H*`OIU_yBZs~zBONOhDVUqFK zhHZ|(DD8CIxymLvTRrBm1|92M3t@HXR%6)TjT>$vw|QoR83Sw`U?@rB;z$(R@`RM(F2 zGgTkvn;of8tFZ1w8( zj|{ZP>E|6|LJWuJiOBXG5m`K+BW=Sqz_@Ae{d|E(UbO3p>jj-XWPO&YfZuws|H%e> z(y0f=h}O4>cFe$=@f4M{*`MoeQsnA|jxlxCW)6(0^XII9@pzuK*#M6?!ndL4r|%leMEFv%Yl?$04co$#>)_FJ{KSz>vFsyl-kUH z*Q>{K0yfF>Wsb4K+K94uFT=|ElJW<5<^38c+Y0cmU2z<3RX6>5O-)SO`lq(VKAHgOOxj#PwY3j;f_Xxtg6<8?De?vreK>D;B7(X_* zsT)*epo~0tRx+XruhxnKpl>7Ki{6|>b}DjIkrlqupv}<$X>+tdS~i_Z?^XJ!A}1BO z0ORdCHq7i#eRwp<<^3V0&xoXDQ+(Ll{P2az&%G-kMK&MtNZK4VekD#jY^$(SxS%S{ zeD>?!6`J`HNL}g`4y~tCWR36P2wNak?|@Xj2hw&QfbrTH+eRahE_4?lRj*#-U%3&E zc;hPVo0G!ftDa7gqrwSDhsyeEo*vKF`F^CZQ`iG<+IRFiGqdyoNb56@cJ1OHz52~h z@mEhcIWYy0};G6%GnV;1}?sQ7hDb)4Rlr0mzF1NQ+?v(jGSf zX+mb;zKfC(6?c2}_$#H>rAA?|F#ndPpS(Y96G+u-Ae~TpAT7n!J>Di^3B3G!imjOs zyy!6rR)~!E8rg_yAa!Ylmo?BaByiVt>08iMWT~)L*eL82_6i4ulfqeHw&Ax;d6)`w zg{8tuVWY5B*a0`symM=7_9}8zI4PVJE(%vChzZFR779y+wZcYWtFTu%C>#~e3KxZ| zLXBNvp|Da|D{K{Z3I~Ow!b#zxFnfX;rouvDrLcIiw;A_X>^5(uuzQL}#)o?Q8mpx|LVOSTt#KM{G;83|Trb0JHw6*j=Q!ETYQikyKlOMWtao)+AH9BKe%VBP!6QCb^)Z$SHOc0 z-IH_)uLZySlXq^lIRPm>f1P*f;&&zKg~C!{t*`-Jmma8F;GPr*g`>h5NS$ARM_%;B ztzj1b86(20r+w7{_r1uUDK%`~cC@9_y5tW1F!xIX4W~ZY#{Pgq|9{8o?P%*< zACc``H84hGkv%X*WH`UW(_@k?eZk)Q)^mI<*>NfVZyp&3D~qiDzvBiXZATb@Z~3)k zDUQH61X<*yu=u*SdDA^VvNg;K82gcRegHG@AWR( z*r#pi2Z3*Tq2I*29}HK(uO99DyA{f}q21N&flr-$vWeB8zYFFb!+q#b15; z)-KZkW0Ebh1;&KCfcbDTXtKc3_m-y_&*A~3#3AdK%346CPNtz#wI z9@hc6`Zl!4;bc#b!>?iWG)GDwfpmslRAhdNr_=ic0^^Hmn~=cxVwy0%nD$A2t+yGw zjP}whVlK5e|+OrmTuLDKj%o>i)Uc;(>8JWS04E){EuD;NRizw9vO?)(g%g3 z!tB#r$adHUNQJV=Bd@#1j}TU<|BS%;Hb+WdecthofAn-4QMV1P&F&75j3bzjeH+^4 zR{M7%a@dA;WEgPm70cVsMtd7 zkXFcy$XFq^7^ZJ~=XXE-i(7?eAa%aZ{Hm9*RXA)zTZ-d0wCc0MZigr|D4Y~73iI#s zHe)GT^+I6z&BvHzCwUhJ%5BKR2}6QyP>6bK-%uZ_ln37 z7*_(8z5ppbd!$HT0V%yySSy@>$3Ojp*dg+Ae5x?)fpOP}Fzy-| z4v4(*AN=+{;RWCDoy%}WBn>lrw~zf8OtwX?fE1Z4tQ0n?&30R)ZOsn&U|b$}=YhvQ z+GpO@XTG1eksX2xg(HwI@@L?+XZUr9T`v{?1&aaq!3-;4jNPzN*aA1+@6Gr%7%)B? z62>MrT=kxI^bxJdp( zHvmt>M`0_JAMollpUnpyV|iO-cCBL^E)4rS9Qo#$!tC!n@{Y~qG|?-}XAznIJqo?n zPyUA;n(7?|@Oa#Su?4nz<{9gMvkUP_#c_{gyzI!*2jJd^`EiNxv||$-5qaRb-g%2G z&+s-M|Ej_Y8aBX~CBs(X1l-YlX=~Zcz*}DIg{<@av$^wz3vlmYJ~4*bnI3sLwt(RZ z7-KigfiWVF{5em*{!8Abb-u^D?CA@&QQ@R;z>j?Rya}W)d?z5?I$pinyY%&!CclEI zfz)OLq&6%3Vb|Nw_hxLEGmt*EWY>5E;RuYaY3bRu9(ni^pRl#z0`J_vv4tzVh@Yk| zmw3GYs`;2}PFUCQ`|~ya1niOcAHDO1N7BXKqHxA9rD>KHAk9*ClDEk-52WX;a^Mkr z{cT0or3Of6?MY#dKUY8#QYx$zHVRvXox(xksBl)eC|teXr;bK6<1e1lm-2!1oqiyF zr=MNyZSH=bzfs>Nxd7gQf`%24zUU9!pGNj7eR!)Ey5&oLN7rvt055vk8Mc!B1bw+j zo_*E@h7Vb<(YbewZwIVP<;NW3YRz85yWD{E^lVuFjpLd4A1%H9tRpS&{%=Kk{&|7T zw;ZFo-DBy1u|9o7_ju%;cl*CSpAzpCg<6HH`?$JY8s*;>>BC|E2HWVTKN${;ep;7W zyz4e1?H+Xxj7a;qx&Y&=jej^a&K;`6E5xp8v+sAj`Y+ErG(TD9m)XGB5ey69wIB8EZ&<3xT193@d!cxO-O_tt?68Ef z!x|2VJQ9O2995g`W4zE+Z}fiJ*oSRs^En;kk+GHx%O7xzwPaW+EOL*GS+d9)7_(&9 z19$&+@|u(ZNGIsPy_Y1Bql%n>N5AT^>l%KBoq?A>+Ph}e7vSkQiW_E+^$5beaEukQ zzJT9R0Aqz1mcSUhVGWG28#XGkQ<259z50IqlJ2?d>g8FEu^(-&u>!`s6f80@b}ozT z5P3A(w#We(Z-6JD% z$aBzN!vYu+Vz>a~_Z^1yTRc6+Zu@2fjIkRQZ^tmvd0VtYAUf~M8yG(*FkHRE)1&i- z^`(vv|81WT!xp$3y)f*7ci~7zNITbr$QZjtE|+_uIM&&SR__*A0%LhwdIgM4Y*?$v zMn(3(ST>fP|DIRBC!NnOFrCjCNb{NP_jH=i>h~RK>N?A38&ey-l* zZC;IIv*8GgYX-ya3XhCo+9XfFC`5P*Hj6K?1D<|S<5z%&B`}6**Z||OX4nFERaZoj!fscPgb?E33f1Gjf$m5Ule;>R)u=K!4H(Xug5%;_)*^6u7sSkR-wP`z7 z2aI(4w7US~kZ$MA)d#&z!X6mu*5;saR5&TDKIDa7bE%)stor<6#~8cKQvMOgxDxP1 z3ydoP!vYxnG@Neq^m8$VKA->HF;<90mY;Ntsk2!s|IBeOnlY?_QHbzSd;KS7hQ&>u zeisTl{;lJ|U-bp{*+YZhQ39h)!xp&f#s2xouIIaL>C-xWxZT^l<#)VI!x^|2Yv1Sd ze|qHY&q~@Xf$<62ehyXvqo4jmJcXUY{);?JZ}T4=&ndm1KJyRrMG!M@*Z@y^!>`&( zHe9Vd^7xPW`=|{IU@Th08W=mQVF!#I)^JvltA~3biY$P!YkPHI94-ti6Sr~^~kf)jJ>))kj`;| zdye&VD-?M0>AsClU3V$)n0F)_Zu&v){KbbpqU@M~`%dr)@vF*XJ@URc`U-i|I6R|*S-rNTyG3yhh!LY;~nRpg{_2EG<|B&^Ns$vz^w|Cs~n zR%Z#k@UncJiF@h5T`9J}`z}o)J0NZM9!SF+wxO-M5lEe%wnf^AW)->IA5!(~DZJ*b z%@vTU=PI(eKcw^$ku)KJ6j`Y@YlV%%78tL@w-E(W^-iT{C#eYmQu+!=ozH=EFFlZd zR;eNjAVqdS+HgIPx-_WBNks#||K-zFKke1D&(zBDj(=?(S__lq?hyp3HP?62kMVsA^3Y-+q z3Kt*^Gu!2D2HIgQ2hzS7$el+dVFjc!Y#>E;Dt%RZm*Rt%EruLOUu70R`YN*m(ywug z^SsT|zM9++u7UIscvM)v$kQouQdquNL^cXXh1L0AdJm*74M6JB2&68xFZV88b4>CzZU>|n7XJR!ue8fGwzf=V!d#u%S81OFHfh%PyuN%)Id4}^+1}C>|%c*JK_8R$Lrsl zysbU(>sKYXAd-%s*#VCrtp4Kc^&DhT=xH|0Rv^83b@iJb$;Txi zMb^NmZiTu?Pv1}52d3}59f0v?2Q9sQz368Lr0N5Z`Wd+Ee{gOOG!yVTPO$Ni3! z{vD(ZcLgFpopfmc?n_5B0%&XOZ~XhD&A?mk^zRL=OFbgb zJ?~xX;$D3O?mIuh>VsZ=-!~GRfVAEFYdw-T9FR8gq%i-Gryn~e^VtJG_j&&%vfa=K z-17w=k>70m6HmWyXEIAI@ZcAdu~(n)Na}nby|p{5-(fRO8!iXZ!KwgW_~)KslUxDm zWLm2>8zAj*qlygNchzUMHr%Yz^IuS%2U2=602e@eDd;Q5z)B-utPasXca ziBE1tj=*<(BWZI2(!N>0*yoe>xE@HS@zf^GAOrnWY>Udz>AYifw4SVYvioxLeOo(t!tdCFv!QKG@E{Sl-t8`BYD%LuLEZjuCn2 z8?8g1CV&xXr^xX%5xF{@+w_y^ZpQ;Z?*BUeEJxbd$LBfHFel(av~7{gy_c{5&91&N zIlpKB?06v#nHISMKI_h8C09U7uYrf(okRxSfhn{$2bDeocVbakE*Y*^9R%PKuWI=NuBS36gdFzo02Y# zDm}~I{jazC3V2JJo&%|R1KgiR22z(=l|BLYyf#@Ofs{V0^kRp1{+Kj9kkU&;Qs+D1 zfqhB!KuYfsdGIw!WFTGe42XQ}tCGl3RiA)#J_@9B$Bali@deUun0=Q|$PM4{HD$X@ z4!keL61eM|Nn{PYFvTX?OtFhLQyikryOTDjXfwqn+DvhEn0NlZ6m#INZzXM(zzb8X zfj6XBKGfT!KZ=y^6xb?U6c!H?>5alc;i9lusWuf33P*+6!$q5=!d7AS-JZ@@0zkSF zD1dw=pdvfqDfmN1wmxTIoFWZ}@8RlphFu-y7=`?r;rlq!(rX}pXae4TFu5bqtH?n` zE-Es6q*tdlbKot9J#p*QlRw%c={lqa(%47f-Me41l|BRcIs|yf&9B~y%pSwDWD^qj z*HU;q1^D^z;$$?b8ROyvUuT}b#U1P(%@ZMza2)yy@&)?ccfnP{($<9bW_D_@a zz=KapK2`_rfBe7OYI9N51F!vl5lPjv9o~5=6i9_uh@^fNz}tT+DO4(~6xIq`g`L7) z;izy@I4fKfuD;7>iH4agEEJXsD~0tov;%ds4Q)T_6!zQD(uZwm>7&9~;i51*Oiaj1 zVWF^8SShR(HVRvXox)z>5SZ>0bI>jUD=sg4J=)HQnhzz{^gumH3R2GP&^a@CkwQ93b>77dNRr;XPXB8Pp zU0PIn{-Zv2iY$OMbtRC-UaRy*rMD`5P?3SurBS6XK#I(EsjUg5&KE#RFI9S_(pwc7 zNNsj1eFReEq}rTSdiD&l;Z{J}a5<31Ua81H>Qb%JJCz4Qq2fD}2aHW!t?D#h4y zAdS5M(%5Si8Ax4fReBGk$U(I^s`Oc%iNRf?dvsLN6N*`4EsL~e|8Ax5q zPE|WBkRnSUZTCv0H!3oa+U!*N0HnxKwK=KuMWtsyCAQ`YNE@yIQuR`$S1P?#k%81^ zr_x6tMNX>CS*2$`t#()-ZMYmrW3N5YnPRhykkA5{9N(kGRk zoh~+9Aa#C)NZN2EkRmJ9X06g&mENiJUZqbeGLX77tMt`wvBTy--kLxfd!^EAmENfI zPNnxMeNgF>N}pBwqSEu9727?KrmjRJjlBj^WTV<_ReG<|2bDgm^hHGmQkSx4svQU^)#M<7K` zs?AxYug(yQHjvsZ5J_XNfD~D)HXD`Rsq|i@4=R0Dk%82uMWyGJ*zN_8wtESrvDYfS zQR%HpA5>%@b$(Ro3y>nSXQ{0Tq|O&WN-tG7N|oNI$X2!4sq{gmk1Bmq>DhC{z8OfJUm=plUIHny zQf<~My;bR*O7B(rq#^^UOS4K}{hV5~K;D`_8hfSEYn9%p^j<{5WQnRr;VJ1F1`sN?(8!nLSsmNBmAke5Kl~fwx@o z*IQp@Ho)VbntZ?60_is+fz+i=6&h5VfmD4&&t)&7;oiA0PKq^!r@{Ug@4+Gb#P@@X9Kx(rCZl;|Nq^avwp;5INNW+{E zxhpLcNQD+vD0_i#4r+4+r1U@1Pk&-u5iP^Sv@Kx%UU(!>9OH1<&ynpK;DG@lD1k4b+G5lDqrFBID-2U42_kkSKb zm?a|Vw-}WwRI5UbDilbCT0~x$4zp8*dR1ruQkx_2K-y*?jeSyu7S(1T&1Y8o%-@j~ z3Zz0gBIyuR0IAIqNa=wz%nFh8E0|gpYE+?C6$+$69U^z7Key>sp+OZIfz;*{k$8cD zU55nH*k@HJ`vsqQYBP}LbA?FyQBoikDiBHAs031*6_C;csY^8?ccnjxYE+?C73x%> zKq}NDl7FS83XQ7J1f(|SX!8}xPh$dU?29V2I!|n)K$_1Skvr30A_r2T5|OlxDj>C4 z11UX_hS?x;S6aPQg*sKJSA_zp(16Izw9u#uO{&lgq&64ef%F$ufi(8)Md~yGq&9OP z&1V5Tm=+48LX|31t2P@Tr3X@%T10NpFTYfwUKJWtp+G7$B62e=G^s+fDzpHp&FsZK z^YpW|KpOiBk+i%EAhj7t+o(k39ckwSsZgy7H9%^!1yXt-b*V$-&etV}i(VBPRH0E7 z3Zz04A~(}QvnsTxLfQH1xCGplwz&e**mEFlqf)gQNb^}Cl75*ONQD|zs0C7+9gxxk zY3h1J(ho2PRcKU&CRHeq3eAY5ABrxjQ1%kv95kX8klM_F^i$2iW7D5J2hxNTNT&@~ zsX~F&r5cgcX0O^Dfw!NS+$0J7>W6%|cEK~NHUl>wm_+6;_5YyG7eH#W1XA@HNSzNn zkQVAyp;5INNY!UmDDYrfD1Vt4Q3<3rDuxbdK5mKq=pvj@`DjX)|i0jbao+)N8C zKq{2KT#X1wg(@Hws(}a6LJg1#4L}|dkP1yeDl`KRriB(D6)JvFjR;7EDj*fAfg6XX z+XzU7dLWMoNQEXK6`FyYX`uy3g^ImuL_jK30jW?8JdhS@fK;dl@`!*`XaZ898F(-) zv;e74@gLNPfK;dgQlSP&Z3b@qn`FZcs?em`45aFdDipYx7Ak&8jHm)qn>CO}1U!(o z*#c>p1CX}S1f)VUkP0opgK42`(>qUv3Lq7#fK;dkQlSR8aYV8?S|Ak~fmCP$QlS}0 zg%;puS}6NvF`^Pkg=!$R8A#Pz)n?#2h-{mBB@XVq|OIYp-vSF+&D7XaFZ&u0IALF6`n@bSHR7*%^XNmR{?oM zKq}M%sZa+zkQVBJRA>THp#?~VvRA4R0S~5yav&9|fmEmgQlS<|BkEO~fg2A=w$ZE# zWv>#Q52WfjBB}F%n`xmMku;(fNNskidJjC1wmAT)`V6E(*{}JCsL%>XQ+$s0C7?4oHQ1;KoCf%`pI}&;q1F*#&AuKq{02H`77|kP09iCBH`8SkxS@~^0uf1vpuo-a za1pqnkdE^aNvEE`&Gd{AxS^2F?-5B?7lE7Ul|bNzLb}+CNV?Pv+)OVE12+`XMSeum zM~uMD^y5I_hC=#q7m@VQGH^5f7#O&rkUqahB;7p-+)O{|*T3~ad)DOKuOu%O3B2f& z$s0TZ|KR;1@`hgEQSVK#L7`K2B(L!ayy4y?vO{FN^u}IT5qNG|C~)_alYRys`+t9E z>p_%WwHdfS9ed!F2a+z;hhJ;6wE4qH=Ud=iH{QBcr~_XAIDxm}{gqBUw)y#K9T#ob6e?w2T~ljRkt<+&%q0I45w|8*3ZDtrELcO z%B?4?GyP4=`4K*K^bVrHH~!N4Z+OK!nGyL{Z}TN-)yoHa`YV1UxnCD}%0FyP^1lFt C(qiub literal 0 HcmV?d00001 diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index 9d529f9b5..ba7eda277 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -39,6 +39,7 @@ z3_add_component(rewriter rewriter.cpp seq_axioms.cpp seq_eq_solver.cpp + seq_subset.cpp seq_rewriter.cpp seq_skolem.cpp th_rewriter.cpp diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 4453c94a7..26455e2f1 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4587,51 +4587,7 @@ bool seq_rewriter::are_complements(expr* r1, expr* r2) const { * basic subset checker. */ bool seq_rewriter::is_subset(expr* r1, expr* r2) const { - // return false; - expr* ra1 = nullptr, *ra2 = nullptr, *ra3 = nullptr; - expr* rb1 = nullptr, *rb2 = nullptr, *rb3 = nullptr; - unsigned la, ua, lb, ub; - if (re().is_complement(r1, ra1) && - re().is_complement(r2, rb1)) { - return is_subset(rb1, ra1); - } - auto is_concat = [&](expr* r, expr*& a, expr*& b, expr*& c) { - return re().is_concat(r, a, b) && re().is_concat(b, b, c); - }; - while (true) { - if (r1 == r2) - return true; - if (re().is_full_seq(r2)) - return true; - if (re().is_dot_plus(r2) && re().get_info(r1).nullable == l_false) - return true; - if (is_concat(r1, ra1, ra2, ra3) && - is_concat(r2, rb1, rb2, rb3) && ra1 == rb1 && ra2 == rb2) { - r1 = ra3; - r2 = rb3; - continue; - } - if (re().is_concat(r1, ra1, ra2) && - re().is_concat(r2, rb1, rb2) && re().is_full_seq(rb1)) { - r1 = ra2; - continue; - } - // r1=ra3{la,ua}ra2, r2=rb3{lb,ub}rb2, ra3=rb3, lb<=la, ua<=ub - if (re().is_concat(r1, ra1, ra2) && re().is_loop(ra1, ra3, la, ua) && - re().is_concat(r2, rb1, rb2) && re().is_loop(rb1, rb3, lb, ub) && - ra3 == rb3 && lb <= la && ua <= ub) { - r1 = ra2; - r2 = rb2; - continue; - } - // ra1=ra3{la,ua}, r2=rb3{lb,ub}, ra3=rb3, lb<=la, ua<=ub - if (re().is_loop(r1, ra3, la, ua) && - re().is_loop(r2, rb3, lb, ub) && - ra3 == rb3 && lb <= la && ua <= ub) { - return true; - } - return false; - } + return m_subset.is_subset(r1, r2); } br_status seq_rewriter::mk_re_union0(expr* a, expr* b, expr_ref& result) { @@ -6163,4 +6119,3 @@ bool seq_rewriter::get_bounds(expr* e, unsigned& low, unsigned& high) { } return low <= high; } - diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 583720911..4ebd770a7 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -23,6 +23,7 @@ Notes: #include "ast/arith_decl_plugin.h" #include "ast/rewriter/rewriter_types.h" #include "ast/rewriter/bool_rewriter.h" +#include "ast/rewriter/seq_subset.h" #include "util/params.h" #include "util/lbool.h" #include "util/sign.h" @@ -128,6 +129,7 @@ class seq_rewriter { }; seq_util m_util; + seq_subset m_subset; arith_util m_autil; bool_rewriter m_br; // re2automaton m_re2aut; @@ -340,7 +342,7 @@ class seq_rewriter { public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): - m_util(m), m_autil(m), m_br(m, p), // m_re2aut(m), + m_util(m), m_subset(m_util.re), m_autil(m), m_br(m, p), // m_re2aut(m), m_op_cache(m), m_es(m), m_lhs(m), m_rhs(m), m_coalesce_chars(true) { } @@ -424,4 +426,3 @@ public: */ lbool some_string_in_re(expr* r, zstring& s); }; - diff --git a/src/ast/rewriter/seq_subset.cpp b/src/ast/rewriter/seq_subset.cpp new file mode 100644 index 000000000..2fc4d1f71 --- /dev/null +++ b/src/ast/rewriter/seq_subset.cpp @@ -0,0 +1,146 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_subset.cpp + +Abstract: + + Heuristic regular-expression subset checks used by seq_rewriter. + +Author: + + Nikolaj Bjorner (nbjorner) 2026-6-8 + +--*/ + +#include "ast/rewriter/seq_subset.h" + +bool seq_subset::is_subset_rec(expr* a, expr* b, unsigned depth) const { + while (true) { + + if (a == b) + return true; + if (m_re.is_empty(a)) + return true; + if (m_re.is_full_seq(b)) + return true; + if (m_re.is_epsilon(a) && m_re.get_info(b).nullable == l_true) + return true; + + if (depth >= m_max_depth) + return false; + + expr* a1 = nullptr, * a2 = nullptr, * b1 = nullptr, * b2 = nullptr; + unsigned la, ua, lb, ub; + + // a ⊆ .+ iff a is non-nullable + if (m_re.is_dot_plus(b) && m_re.get_info(a).nullable == l_false) + return true; + + // a ⊆ a* + if (m_re.is_star(b, b1) && is_subset_rec(a, b1, depth)) + return true; + + // e ⊆ a* + if (m_re.is_epsilon(a) && m_re.is_star(b, b1)) + return true; + + // R ⊆ R* + if (m_re.is_star(b, b1) && is_subset_rec(a, b1, depth + 1)) + return true; + + // R1* ⊆ R2* if R1 ⊆ R2 + if (m_re.is_star(a, a1) && m_re.is_star(b, b1) && is_subset_rec(a1, b1, depth + 1)) + return true; + + // R1+ ⊆ R2+ if R1 ⊆ R2 + if (m_re.is_plus(a, a1) && m_re.is_plus(b, b1) && is_subset_rec(a1, b1, depth)) + return true; + + // R ⊆ R+ + if (m_re.is_plus(b, b1) && is_subset_rec(a, b1, depth)) + return true; + + // R+ ⊆ R* + if (m_re.is_plus(a, a1) && m_re.is_star(b, b1) && is_subset_rec(a1, b1, depth + 1)) + return true; + + // range containment + if (m_re.is_range(a, la, ua) && m_re.is_range(b, lb, ub) && lb <= la && ua <= ub) + return true; + + // to_re(s) ⊆ range + if (m_re.is_to_re(a, a1) && m_re.is_range(b, lb, ub) && is_app(a1)) { + func_decl* f = to_app(a1)->get_decl(); + if (f->get_decl_kind() == OP_STRING_CONST && f->get_num_parameters() == 1) { + zstring const& s = f->get_parameter(0).get_zstring(); + if (s.length() == 1 && lb <= s[0] && s[0] <= ub) + return true; + } + } + + // a ⊆ b1 ∪ b2 if a ⊆ b1 or a ⊆ b2 + if (m_re.is_union(b, b1, b2) && (is_subset_rec(a, b1, depth + 1) || is_subset_rec(a, b2, depth + 1))) + return true; + + // a1 ∪ a2 ⊆ b if a1 ⊆ b and a2 ⊆ b + if (m_re.is_union(a, a1, a2) && is_subset_rec(a1, b, depth + 1) && is_subset_rec(a2, b, depth + 1)) + return true; + + // a1 ∩ a2 ⊆ b if a1 ⊆ b or a2 ⊆ b + if (m_re.is_intersection(a, a1, a2) && (is_subset_rec(a1, b, depth + 1) || is_subset_rec(a2, b, depth + 1))) + return true; + + // a ⊆ b1 ∩ b2 if a ⊆ b1 and a ⊆ b2 + if (m_re.is_intersection(b, b1, b2) && is_subset_rec(a, b1, depth + 1) && is_subset_rec(a, b2, depth + 1)) + return true; + + // R{la,ua} ⊆ R'{lb,ub} if R ⊆ R', lb<=la, ua<=ub + if (m_re.is_loop(a, a1, la, ua) && + m_re.is_loop(b, b1, lb, ub) && + lb <= la && ua <= ub && is_subset_rec(a1, b1, depth + 1)) { + return true; + } + + // a1 \ a2 ⊆ b if a1 ⊆ b + if (m_re.is_diff(a, a1, a2) && is_subset_rec(a1, b, depth + 1)) + return true; + + // R ⊆ Σ*·R' if R ⊆ R' + if (m_re.is_concat(b, b1, b2) && m_re.is_full_seq(b1) && is_subset_rec(a, b2, depth)) + return true; + + // R ⊆ R'·Σ* if R ⊆ R' + if (m_re.is_concat(b, b1, b2) && m_re.is_full_seq(b2) && is_subset_rec(a, b1, depth)) + return true; + + // star absorption: R·R* ⊆ R*, R*·R ⊆ R* + bool const is_concat_star = m_re.is_concat(a, a1, a2) && m_re.is_star(b, b1); + if (is_concat_star && + is_subset_rec(a1, b1, depth + 1) && is_subset_rec(a2, b, depth + 1)) + return true; + if (is_concat_star && + is_subset_rec(a2, b1, depth + 1) && is_subset_rec(a1, b, depth + 1)) + return true; + + // concat monotonicity: + // tail-recursive on second arguments (without increasing depth bound). + if (m_re.is_concat(a, a1, a2) && m_re.is_concat(b, b1, b2) && is_subset_rec(a1, b1, depth + 1)) { + a = a2; + b = b2; + continue; + } + + // complement: ~a ⊆ ~b if b ⊆ a + if (m_re.is_complement(a, a1) && m_re.is_complement(b, b1)) + return is_subset_rec(b1, a1, depth + 1); + + return false; + } +} + +bool seq_subset::is_subset(expr* a, expr* b) const { + return is_subset_rec(a, b, 0); +} diff --git a/src/ast/rewriter/seq_subset.h b/src/ast/rewriter/seq_subset.h new file mode 100644 index 000000000..7329c898e --- /dev/null +++ b/src/ast/rewriter/seq_subset.h @@ -0,0 +1,30 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_subset.h + +Abstract: + + Heuristic regular-expression subset checks used by seq_rewriter. + +Author: + + Nikolaj Bjorner (nbjorner) 2026-6-8 + +--*/ +#pragma once + +#include "ast/seq_decl_plugin.h" + +class seq_subset { + seq_util::rex& m_re; + static constexpr unsigned m_max_depth = 3; + + bool is_subset_rec(expr* a, expr* b, unsigned depth) const; + +public: + explicit seq_subset(seq_util::rex& re) : m_re(re) {} + bool is_subset(expr* a, expr* b) const; +}; From d415ead6a234d6374e15b09c932f03787741eb0d Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 9 Jun 2026 14:35:48 -0700 Subject: [PATCH 13/14] Port `is_classical` attribute to `seq_util::rex::info` (#9796) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `is_classical` (tracks whether a regex uses only classical operators — no complement, intersection, diff, or empty-language/fail) was only available on `euf::snode`. Moving it into `seq_util::rex::info` makes it accessible to all regex-handling code without going through the snode layer. ### Changes **`seq_decl_plugin.h`** - Added `bool classical { true }` to `seq_util::rex::info` - The general `info` constructor requires `bool is_classical` explicitly (no default) **`seq_decl_plugin.cpp`** - `mk_info_rec`: `OP_RE_EMPTY_SET` (fail) sets `classical=false` - `mk_info_rec`: `OP_RE_RANGE`, `OP_RE_FULL_CHAR_SET`, `OP_RE_OF_PRED` set `classical=false` - `complement()`, `conj()` (intersection), `diff()`: always produce `classical=false` - `star()`, `plus()`, `opt()`, `concat()`, `disj()`, `orelse()`, `loop()`: propagate `classical` via logical AND over operands - `operator=` and `display()` updated to include `classical` ### Semantics | Operation | `classical` | |-----------|-------------| | `re.empty` (fail) | `false` | | `re.range`, `re.allchar`, `re.of.pred` | `false` | | `re.comp` (complement) | `false` | | `re.inter` (intersection) | `false` | | `re.diff` | `false` | | `re.all` (full sequence set) | `true` | | `str.to.re` (string literal) | `true` | | `re.*`, `re.+`, `re.opt`, `re.++`, `re.union`, `re.loop` | inherited from operands | --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/ast/seq_decl_plugin.cpp | 37 ++++++++++++++++++++++--------------- src/ast/seq_decl_plugin.h | 8 ++++++-- 2 files changed, 28 insertions(+), 17 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 634ced5c9..8986e7ec1 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1653,9 +1653,9 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { if (e->get_family_id() == u.get_family_id()) { switch (e->get_decl()->get_decl_kind()) { case OP_RE_EMPTY_SET: - return info(true, l_false, UINT_MAX); + return info(true, l_false, UINT_MAX, false); case OP_RE_FULL_SEQ_SET: - return info(true, l_true, 0); + return info(true, l_true, 0, true); case OP_RE_STAR: i1 = get_info_rec(e->get_arg(0)); return i1.star(); @@ -1667,7 +1667,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { case OP_RE_OF_PRED: //TBD: check if the character predicate contains uninterpreted symbols or is nonground or is unsat //TBD: check if the range is unsat - return info(true, l_false, 1); + return info(true, l_false, 1, false); case OP_RE_CONCAT: i1 = get_info_rec(e->get_arg(0)); i2 = get_info_rec(e->get_arg(1)); @@ -1684,7 +1684,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { min_length = u.str.min_length(e->get_arg(0)); is_value = m.is_value(e->get_arg(0)); nullable = (is_value && min_length == 0 ? l_true : (min_length > 0 ? l_false : l_undef)); - return info(is_value, nullable, min_length); + return info(is_value, nullable, min_length, true); case OP_RE_REVERSE: return get_info_rec(e->get_arg(0)); case OP_RE_PLUS: @@ -1720,7 +1720,8 @@ std::ostream& seq_util::rex::info::display(std::ostream& out) const { if (is_known()) { out << "info(" << "nullable=" << (nullable == l_true ? "T" : (nullable == l_false ? "F" : "U")) << ", " - << "min_length=" << min_length << ")"; + << "min_length=" << min_length << ", " + << "classical=" << (classical ? "T" : "F") << ")"; } else if (is_valid()) out << "UNKNOWN"; @@ -1740,13 +1741,13 @@ std::string seq_util::rex::info::str() const { seq_util::rex::info seq_util::rex::info::star() const { //if is_known() is false then all mentioned properties will remain false - return seq_util::rex::info(interpreted, l_true, 0); + return seq_util::rex::info(interpreted, l_true, 0, classical); } seq_util::rex::info seq_util::rex::info::plus() const { if (is_known()) { //plus never occurs in a normalized regex - return info(interpreted, nullable, min_length); + return info(interpreted, nullable, min_length, classical); } else return *this; @@ -1755,14 +1756,14 @@ seq_util::rex::info seq_util::rex::info::plus() const { seq_util::rex::info seq_util::rex::info::opt() const { // if is_known() is false then all mentioned properties will remain false // optional construct never occurs in a normalized regex - return seq_util::rex::info(interpreted, l_true, 0); + return seq_util::rex::info(interpreted, l_true, 0, classical); } seq_util::rex::info seq_util::rex::info::complement() const { if (is_known()) { lbool compl_nullable = (nullable == l_true ? l_false : (nullable == l_false ? l_true : l_undef)); unsigned compl_min_length = (compl_nullable == l_false ? 1 : 0); - return info(interpreted, compl_nullable, compl_min_length); + return info(interpreted, compl_nullable, compl_min_length, false); } else return *this; @@ -1776,7 +1777,8 @@ seq_util::rex::info seq_util::rex::info::concat(seq_util::rex::info const& rhs, m = UINT_MAX; return info(interpreted && rhs.interpreted, ((nullable == l_false || rhs.nullable == l_false) ? l_false : ((nullable == l_true && rhs.nullable == l_true) ? l_true : l_undef)), - m); + m, + classical && rhs.classical); } else return rhs; @@ -1790,7 +1792,8 @@ seq_util::rex::info seq_util::rex::info::disj(seq_util::rex::info const& rhs) co //works correctly if one of the arguments is unknown return info(interpreted && rhs.interpreted, ((nullable == l_true || rhs.nullable == l_true) ? l_true : ((nullable == l_false && rhs.nullable == l_false) ? l_false : l_undef)), - std::min(min_length, rhs.min_length)); + std::min(min_length, rhs.min_length), + classical && rhs.classical); } else return rhs; @@ -1801,7 +1804,8 @@ seq_util::rex::info seq_util::rex::info::conj(seq_util::rex::info const& rhs) co if (rhs.is_known()) { return info(interpreted && rhs.interpreted, ((nullable == l_true && rhs.nullable == l_true) ? l_true : ((nullable == l_false || rhs.nullable == l_false) ? l_false : l_undef)), - std::max(min_length, rhs.min_length)); + std::max(min_length, rhs.min_length), + false); } else return rhs; @@ -1815,7 +1819,8 @@ seq_util::rex::info seq_util::rex::info::diff(seq_util::rex::info const& rhs) co if (rhs.is_known()) { return info(interpreted & rhs.interpreted, ((nullable == l_true && rhs.nullable == l_false) ? l_true : ((nullable == l_false || rhs.nullable == l_false) ? l_false : l_undef)), - std::max(min_length, rhs.min_length)); + std::max(min_length, rhs.min_length), + false); } else return rhs; @@ -1832,7 +1837,8 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co // TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted return info(false, ((nullable == l_true && i.nullable == l_true) ? l_true : ((nullable == l_false && i.nullable == l_false) ? l_false : l_undef)), - std::min(min_length, i.min_length)); + std::min(min_length, i.min_length), + classical && i.classical); } else return i; @@ -1848,7 +1854,7 @@ seq_util::rex::info seq_util::rex::info::loop(unsigned lower, unsigned upper) co if (m > 0 && (m < min_length || m < lower)) m = UINT_MAX; lbool loop_nullable = (nullable == l_true || lower == 0 ? l_true : nullable); - return info(interpreted, loop_nullable, m); + return info(interpreted, loop_nullable, m, classical); } else return *this; @@ -1863,6 +1869,7 @@ seq_util::rex::info& seq_util::rex::info::operator=(info const& other) { interpreted = other.interpreted; nullable = other.nullable; min_length = other.min_length; + classical = other.classical; return *this; } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 78ad6d544..756ec38e4 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -443,6 +443,8 @@ public: lbool nullable { l_undef }; /* Lower bound on the length of all accepted words. */ unsigned min_length { 0 }; + /* Classical regular expression: does not use complement, intersection, diff, or the empty language (fail). */ + bool classical { true }; /* Default constructor of invalid info. @@ -459,11 +461,13 @@ public: */ info(bool is_interpreted, lbool is_nullable, - unsigned min_l) : + unsigned min_l, + bool is_classical) : known(l_true), interpreted(is_interpreted), nullable(is_nullable), - min_length(min_l) {} + min_length(min_l), + classical(is_classical) {} /* Appends a string representation of the info into the stream. From e093be8b607d255373402bd8f52554cd0dd504ba Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 9 Jun 2026 14:38:38 -0700 Subject: [PATCH 14/14] seq_rewriter: add missing concat rewrites for nullable/full-seq/star cases (#9782) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `seq_rewriter.cpp` was missing several regex-concat normalizations around `re.all` (`Σ*`), causing avoidable growth and missed simplifications. This update fills the four gaps: nullable absorption, guarded union distribution, intersection suffix elimination, and nested-star collapse. - **Nullable/full-seq absorption (A1)** - Generalizes `Σ*·R → Σ*` and `R·Σ* → Σ*` beyond `Σ*·Σ*`. - Applies when `R` is interpreted, nullable, and has `min_length = 0`. - **Guarded distribution over union (A2)** - Adds `Σ*·(R1 ∪ R2)` distribution when at least one arm is already `Σ*`-headed. - Rebuilds via normalized union so the redundant arm collapses to `Σ*`. - **Intersection + full-seq tail elimination (A3)** - Adds `(R1 ∩ … ∩ Rn)·Σ* → (R1 ∩ … ∩ Rn)` when every intersection leaf already ends in `Σ*`. - **Nested star concat collapse (A4)** - Adds `R*·(R*·X) → R*·X`, covering non-adjacent star patterns not handled by the prior adjacent-only rewrite. ```cpp if (re().is_full_seq(a) && accepts_empty_word(b)) result = a; // A1 if (re().is_full_seq(a) && re().is_union(b, u1, u2) && ...) ... // A2 if (re().is_intersection(a, u1, u2) && re().is_full_seq(b) && ...) result=a; // A3 if (re().is_star(a, a1) && re().is_concat(b, b1, b2) && re().is_star(b1,b3) && a1==b3) result=b; // A4 ``` Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/ast/rewriter/seq_rewriter.cpp | 58 ++++++++++++++++++++++++++++++- 1 file changed, 57 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 26455e2f1..46da49cf2 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4491,10 +4491,60 @@ br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) { r* ++ r -> r ++ r* */ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) { + auto accepts_empty_word = [&](expr* r) { + auto info = re().get_info(r); + return info.interpreted && info.nullable == l_true && info.min_length == 0; + }; + auto starts_with_full_seq = [&](expr* r) { + expr* r1 = nullptr, *r2 = nullptr; + return re().is_full_seq(r) || (re().is_concat(r, r1, r2) && re().is_full_seq(r1)); + }; + auto ends_with_full_seq = [&](expr* r) { + expr* r1 = nullptr, *r2 = nullptr; + while (re().is_concat(r, r1, r2)) + r = r2; + return re().is_full_seq(r); + }; + auto all_inter_arms_end_with_full_seq = [&](expr* r) { + ptr_buffer todo; + todo.push_back(r); + while (!todo.empty()) { + expr* r1 = nullptr, *r2 = nullptr; + expr* t = todo.back(); + todo.pop_back(); + if (re().is_intersection(t, r1, r2)) { + todo.push_back(r1); + todo.push_back(r2); + } + else if (!ends_with_full_seq(t)) { + return false; + } + } + return true; + }; if (re().is_full_seq(a) && re().is_full_seq(b)) { result = a; return BR_DONE; } + if (re().is_full_seq(a) && accepts_empty_word(b)) { + result = a; + return BR_DONE; + } + if (re().is_full_seq(b) && accepts_empty_word(a)) { + result = b; + return BR_DONE; + } + expr* u1 = nullptr, *u2 = nullptr; + if (re().is_full_seq(a) && re().is_union(b, u1, u2) && + (starts_with_full_seq(u1) || starts_with_full_seq(u2))) { + result = mk_regex_union_normalize(mk_regex_concat(a, u1), mk_regex_concat(a, u2)); + return BR_REWRITE2; + } + if (re().is_intersection(a, u1, u2) && re().is_full_seq(b) && + all_inter_arms_end_with_full_seq(a)) { + result = a; + return BR_DONE; + } if (re().is_empty(a)) { result = a; return BR_DONE; @@ -4525,7 +4575,8 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) { result = re().mk_to_re(str().mk_concat(a_str, b_str)); return BR_REWRITE2; } - expr* a1 = nullptr, *b1 = nullptr; + expr* a1 = nullptr; + expr* b1 = nullptr; if (re().is_to_re(a, a1) && re().is_to_re(b, b1)) { result = re().mk_to_re(str().mk_concat(a1, b1)); return BR_DONE; @@ -4534,6 +4585,11 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) { result = a; return BR_DONE; } + expr* b2 = nullptr, *b3 = nullptr; + if (re().is_star(a, a1) && re().is_concat(b, b1, b2) && re().is_star(b1, b3) && a1 == b3) { + result = b; + return BR_DONE; + } if (re().is_star(a, a1) && a1 == b) { result = re().mk_concat(b, a); return BR_DONE;