Merge branch 'Z3Prover:master' into parallel-solving

.github/copilot-instructions.md

@@ -0,0 +1,167 @@
+# Z3 Theorem Prover Development Guide
+
+Always reference these instructions first and fallback to search or bash commands only when you encounter unexpected information that does not match the info here.
+
+## Working Effectively
+
+### Bootstrap and Build the Repository
+
+Z3 supports multiple build systems. **ALWAYS** use one of these validated approaches:
+
+#### Option 1: Python Build System (Recommended for most use cases)
+- `python scripts/mk_make.py` -- takes 7 seconds to configure
+- `cd build && make -j$(nproc)` -- takes 15 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes.
+
+#### Option 2: CMake Build System (Recommended for integration)
+- Clean source tree first if you previously used Python build: `git clean -fx src/`
+- `mkdir build && cd build`
+- `cmake ..` -- takes 1 second to configure
+- `make -j$(nproc)` -- takes 17 minutes to complete. **NEVER CANCEL**. Set timeout to 30+ minutes.
+
+#### Dependencies and Requirements
+- Python 3.x (required for both build systems)
+- C++20 capable compiler (g++ or clang++)
+- GNU Make
+- Git (for version information)
+
+### Test the Repository
+
+**Python Build System:**
+- Build unit tests: `make test` -- takes 3.5 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes.
+- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes.
+
+**CMake Build System:**
+- Build unit tests: `make test-z3` -- takes 4 minutes to compile. **NEVER CANCEL**. Set timeout to 10+ minutes.
+- Run unit tests: `./test-z3 /a` -- takes 16 seconds. **NEVER CANCEL**. Set timeout to 5+ minutes.
+
+**Test basic Z3 functionality:**
+```bash
+./z3 --version
+echo "(declare-const x Int)(assert (> x 0))(check-sat)(get-model)" | ./z3 -in
+```
+
+### Validation Scenarios
+
+**ALWAYS** test these scenarios after making changes:
+
+#### Basic SMT Solving
+```bash
+cd build
+echo "(declare-const x Int)
+(assert (> x 0))
+(check-sat)
+(get-model)" | ./z3 -in
+```
+Expected output: `sat` followed by a model showing `x = 1` or similar.
+
+#### Python Bindings
+```bash
+cd build/python
+python3 -c "import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())"
+```
+Expected output: `Result: sat` and `Model: [x = 1]` or similar.
+
+#### Command Line Help
+```bash
+./z3 --help | head -10
+```
+Should display version and usage information.
+
+## Build System Details
+
+### Python Build System
+- Configuration: `python scripts/mk_make.py` (7 seconds)
+- Main build: `cd build && make -j$(nproc)` (15 minutes)
+- Test build: `make test` (3.5 minutes)
+- Generates build files in `build/` directory
+- Creates Python bindings in `build/python/`
+- **Warning**: Generates files in source tree that must be cleaned before using CMake
+
+### CMake Build System  
+- Clean first: `git clean -fx src/` (if switching from Python build)
+- Configuration: `cmake ..` (1 second)
+- Main build: `make -j$(nproc)` (17 minutes)
+- **Advantages**: Clean build tree, no source pollution, better for integration
+- **Recommended for**: IDE integration, package management, deployment
+
+### Critical Timing and Timeout Requirements
+
+**NEVER CANCEL these operations**:
+- `make -j$(nproc)` builds: 15-17 minutes. **Set timeout to 30+ minutes minimum**.
+- `make test` or `make test-z3` compilation: 3.5-4 minutes. **Set timeout to 10+ minutes**.
+- Unit test execution: 16 seconds. **Set timeout to 5+ minutes**.
+
+**Always wait for completion**. Z3 is a complex theorem prover with extensive code generation and builds may appear to hang but are actually progressing.
+
+## Repository Structure
+
+### Key Directories
+- `src/` - Main source code organized by components (ast, smt, sat, etc.)
+- `examples/` - Language binding examples (C, C++, Python, Java, .NET, etc.)
+- `scripts/` - Build scripts and utilities
+- `.github/workflows/` - CI/CD pipeline definitions
+- `cmake/` - CMake configuration files
+
+### Important Files
+- `README.md` - Main documentation and build instructions
+- `README-CMake.md` - Detailed CMake build documentation  
+- `configure` - Wrapper script around `scripts/mk_make.py`
+- `CMakeLists.txt` - Main CMake configuration
+- `scripts/mk_make.py` - Python build system entry point
+
+## Common Tasks and Validation
+
+### Pre-commit Validation
+Before committing changes:
+1. **Build successfully**: Use one of the validated build commands above
+2. **Run unit tests**: `./test-z3 /a` must pass
+3. **Test basic functionality**: Run validation scenarios above
+4. **Test affected language bindings**: If modifying API, test relevant examples
+
+### Working with Language Bindings
+- **Python**: Located in `build/python/`, test with validation scenario above
+- **C/C++**: Examples in `examples/c/` and `examples/c++/`
+  - Compile C++ example: `g++ -I src/api -I src/api/c++ examples/c++/example.cpp -L build -lz3 -o test_example`
+  - Run with: `LD_LIBRARY_PATH=build ./test_example`
+- **Java**: Build with `python scripts/mk_make.py --java`, examples in `examples/java/`
+- **C#/.NET**: Build with `python scripts/mk_make.py --dotnet`, examples in `examples/dotnet/`
+
+### Performance Testing
+For performance-sensitive changes:
+- Build optimized: `python scripts/mk_make.py` (Release mode by default)
+- Test with realistic SMT problems from `examples/SMT-LIB2/`
+- Use Z3's built-in statistics: `z3 -st problem.smt2`
+
+## Common Issues and Solutions
+
+### Build System Conflicts
+- **Error**: CMake complains about polluted source tree
+- **Solution**: Run `git clean -fx src/` to remove Python build artifacts
+
+### Python Import Errors
+- **Error**: `import z3` fails
+- **Solution**: Ensure you're in `build/python/` directory or add it to `PYTHONPATH`
+
+### Missing Dependencies
+- **Error**: Compiler not found or version too old
+- **Solution**: Z3 requires C++20. Install g++ 10+ or clang++ 10+
+
+### Long Build Times
+- **Normal**: 15-17 minute builds are expected for Z3
+- **Never cancel**: Set timeouts appropriately and wait for completion
+- **Optimization**: Use `make -j$(nproc)` for parallel compilation
+
+## Key Projects in Codebase
+
+Z3 is organized into several key components:
+
+- **Core SMT**: `src/smt/` - Main SMT solver engine
+- **SAT Solver**: `src/sat/` - Underlying boolean satisfiability solver  
+- **Theories**: Various theory solvers (arithmetic, arrays, bit-vectors, etc.)
+- **Abstract Syntax Trees**: `src/ast/` - Expression representation and manipulation
+- **Tactics**: `src/tactic/` - Configurable solving strategies
+- **API**: `src/api/` - Public C API and language bindings
+- **Parsers**: SMT-LIB2, Dimacs, and other input format parsers
+- **Model Generation**: Creating and manipulating satisfying assignments
+
+The architecture is modular with clean separation between the core solver, theory plugins, and user interfaces.

.github/workflows/Windows.yml

@@ -22,7 +22,7 @@ jobs:
     runs-on: windows-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
       - name: Add msbuild to PATH
         uses: microsoft/setup-msbuild@v2
       - run: |

.github/workflows/android-build.yml

@@ -21,7 +21,7 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@v4
+      uses: actions/checkout@v5
 
     - name: Configure CMake and build
       run:  |

.github/workflows/cross-build.yml

@@ -19,7 +19,7 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@v4
+      uses: actions/checkout@v5
 
     - name: Install cross build tools
       run:  apt update && apt install -y ninja-build cmake python3 g++-11-${{ matrix.arch }}-linux-gnu

.github/workflows/labeller.yml

@@ -13,7 +13,7 @@ jobs:
   genai-issue-labeller:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v5
       - uses: pelikhan/action-genai-issue-labeller@v0
         with:
           github_token: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/msvc-static-build-clang-cl.yml

@@ -14,7 +14,7 @@ jobs:
       BUILD_TYPE: Release
     steps:
     - name: Checkout Repo
-      uses: actions/checkout@v4
+      uses: actions/checkout@v5
   
     - name: Build
       run: |

.github/workflows/msvc-static-build.yml

@@ -14,7 +14,7 @@ jobs:
       BUILD_TYPE: Release
     steps:
     - name: Checkout Repo
-      uses: actions/checkout@v4
+      uses: actions/checkout@v5
   
     - name: Build
       run: |

.github/workflows/ocaml.yaml

@@ -17,7 +17,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       # Cache ccache (shared across runs)
       - name: Cache ccache

.github/workflows/prd.yml

@@ -13,7 +13,7 @@ jobs:
   generate-pull-request-description:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v5
       - uses: pelikhan/action-genai-pull-request-descriptor@v0
         with:
           github_token: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/pyodide.yml

@@ -19,7 +19,7 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@v4
+      uses: actions/checkout@v5
 
     - name: Setup packages
       run: sudo apt-get update && sudo apt-get install -y python3-dev python3-pip python3-venv 

.github/workflows/wasm-release.yml

@@ -21,7 +21,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Setup node
         uses: actions/setup-node@v4

.github/workflows/wasm.yml

@@ -21,7 +21,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v4
+        uses: actions/checkout@v5
 
       - name: Setup node
         uses: actions/setup-node@v4

.github/workflows/wip.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-    - uses: actions/checkout@v4
+    - uses: actions/checkout@v5
 
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}}

CMakeLists.txt

@@ -2,7 +2,12 @@
 cmake_minimum_required(VERSION 3.16)
 
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.15.3.0 LANGUAGES CXX)
+
+# Read version from VERSION.txt file
+file(READ "${CMAKE_CURRENT_SOURCE_DIR}/VERSION.txt" Z3_VERSION_FROM_FILE)
+string(STRIP "${Z3_VERSION_FROM_FILE}" Z3_VERSION_FROM_FILE)
+
+project(Z3 VERSION ${Z3_VERSION_FROM_FILE} LANGUAGES CXX)
 
 ################################################################################
 # Project version

MODULE.bazel

@@ -1,6 +1,6 @@
 module(
     name = "z3",
-    version = "4.15.3",
+    version = "4.16.0",  # TODO: Read from VERSION.txt - currently manual sync required
     bazel_compatibility = [">=7.0.0"],
 )
 

VERSION.txt

@@ -0,0 +1 @@
+4.15.4.0

azure-pipelines.yml

@@ -56,15 +56,6 @@ jobs:
   - script: "pip install build git+https://github.com/rhelmot/auditwheel"
   - script: "cd src/api/python && python -m build && AUDITWHEEL_PLAT= auditwheel repair --best-plat dist/*.whl && cd ../../.."
   - script: "pip install ./src/api/python/wheelhouse/*.whl && python - <src/api/python/z3test.py z3 && python - <src/api/python/z3test.py z3num"
-  - task: CopyFiles@2
-    inputs:
-      sourceFolder: src/api/python/wheelhouse
-      contents: '*.whl'
-      targetFolder: $(Build.ArtifactStagingDirectory)
-  - task: PublishPipelineArtifact@0
-    inputs:
-      artifactName: 'ManyLinuxPythonBuildAMD64'
-      targetPath: $(Build.ArtifactStagingDirectory)   
 
 - job: ManyLinuxPythonBuildArm64
   timeoutInMinutes: 90

scripts/mk_project.py

@@ -8,7 +8,20 @@
 from mk_util import *
 
 def init_version():
-    set_version(4, 15, 3, 0) # express a default build version or pick up ci build version
+    # Read version from VERSION.txt file
+    version_file_path = os.path.join(os.path.dirname(os.path.dirname(__file__)), 'VERSION.txt')
+    try:
+        with open(version_file_path, 'r') as f:
+            version_str = f.read().strip()
+        version_parts = version_str.split('.')
+        if len(version_parts) >= 4:
+            major, minor, build, tweak = int(version_parts[0]), int(version_parts[1]), int(version_parts[2]), int(version_parts[3])
+        else:
+            major, minor, build, tweak = int(version_parts[0]), int(version_parts[1]), int(version_parts[2]), 0
+        set_version(major, minor, build, tweak)
+    except (IOError, ValueError) as e:
+        print(f"Warning: Could not read version from VERSION.txt: {e}")
+        set_version(4, 15, 4, 0)  # fallback to default version
     
 # Z3 Project definition
 def init_project_def():

scripts/nightly.yaml

@@ -1,10 +1,12 @@
 variables:
+  # Version components read from VERSION.txt (updated manually when VERSION.txt changes)
   Major: '4'
-  Minor: '15'
-  Patch: '3'
+  Minor: '16'
+  Patch: '0'
   ReleaseVersion: $(Major).$(Minor).$(Patch)
   AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
   NightlyVersion: $(AssemblyVersion)-$(Build.buildId)
+  # TODO: Auto-read from VERSION.txt when Azure DevOps supports it better
 
 stages:
 - stage: Build
@@ -471,49 +473,12 @@ stages:
         tagSource: 'userSpecifiedTag'
         tag: 'Nightly'
         title: 'Nightly'
-        releaseNotesSource: 'input'
+        releaseNotesSource: 'inline'
         releaseNotes: 'nightly build'
         assets: 'tmp/*'
         assetUploadMode: 'replace'
         isDraft: false
         isPreRelease: true
 
-- stage: NugetPublishNightly
-  jobs:
-   # Publish to nightly feed on Azure
-  - job: NuGetPublishNightly
-    displayName: "Push nuget packages to Azure Feed"
-    steps:
-    - task: NuGetAuthenticate@0
-      displayName: 'NuGet Authenticate'
-    - task: NuGetToolInstaller@0
-      inputs:
-        versionSpec: 5.x
-        checkLatest: false
-    - task: DownloadPipelineArtifact@2
-      displayName: 'Download NuGet x86 Package'
-      inputs:
-        artifact: 'NuGet32'
-        path: $(Agent.TempDirectory)/x86
-    - task: DownloadPipelineArtifact@2
-      displayName: 'Download NuGet x64 Package'
-      inputs:
-        artifact: 'NuGet'
-        path: $(Agent.TempDirectory)/x64
-    - task: NuGetCommand@2
-      displayName: 'NuGet Nightly x64 push'
-      inputs:
-        command: push
-        publishVstsFeed: 'Z3Build/Z3-Nightly-Builds'
-        packagesToPush: $(Agent.TempDirectory)/x64/*.nupkg
-        allowPackageConflicts: true
-    - task: NuGetCommand@2
-      displayName: 'NuGet Nightly x86 push'
-      inputs:
-        command: push
-        publishVstsFeed: 'Z3Build/Z3-Nightly-Builds'
-        packagesToPush: $(Agent.TempDirectory)/x86/*.nupkg
-        allowPackageConflicts: true
-    
-       
+
 # TBD: run regression tests on generated binaries.

scripts/release.yml

@@ -6,7 +6,7 @@
 trigger: none
 
 variables:
-  ReleaseVersion: '4.15.3'
+  ReleaseVersion: '4.16.0'  # TODO: Auto-read from VERSION.txt when Azure DevOps supports it better
 
 stages:
 
@@ -492,7 +492,7 @@ stages:
 
   # Enable on release:
   - job: PyPIPublish
-    condition: eq(0,1)
+    condition: eq(1,1)
     displayName: "Publish to PyPI"
     pool:
       vmImage: "ubuntu-latest"

scripts/update_version.py

@@ -0,0 +1,139 @@
+#!/usr/bin/env python3
+"""
+Helper script to update version in all Z3 files when VERSION.txt changes.
+
+This script reads VERSION.txt and updates the remaining hardcoded version references
+that cannot be automatically read from VERSION.txt due to limitations in their
+respective build systems.
+
+Usage: python scripts/update_version.py
+"""
+
+import os
+import re
+import sys
+
+def read_version():
+    """Read version from VERSION.txt file."""
+    script_dir = os.path.dirname(os.path.abspath(__file__))
+    version_file = os.path.join(os.path.dirname(script_dir), 'VERSION.txt')
+    
+    try:
+        with open(version_file, 'r') as f:
+            version = f.read().strip()
+        return version
+    except IOError as e:
+        print(f"Error reading VERSION.txt: {e}")
+        sys.exit(1)
+
+def update_bazel_module(version):
+    """Update MODULE.bazel with the version."""
+    script_dir = os.path.dirname(os.path.abspath(__file__))
+    module_file = os.path.join(os.path.dirname(script_dir), 'MODULE.bazel')
+    
+    # Extract major.minor.patch from major.minor.patch.tweak
+    version_parts = version.split('.')
+    if len(version_parts) >= 3:
+        bazel_version = f"{version_parts[0]}.{version_parts[1]}.{version_parts[2]}"
+    else:
+        bazel_version = version
+    
+    try:
+        with open(module_file, 'r') as f:
+            content = f.read()
+        
+        # Update version line in module() block only
+        content = re.sub(
+            r'(module\([^)]*?\s+version\s*=\s*")[^"]*(".*?)',
+            r'\g<1>' + bazel_version + r'\g<2>',
+            content,
+            flags=re.DOTALL
+        )
+        
+        with open(module_file, 'w') as f:
+            f.write(content)
+        
+        print(f"Updated MODULE.bazel version to {bazel_version}")
+    except IOError as e:
+        print(f"Error updating MODULE.bazel: {e}")
+
+def update_nightly_yaml(version):
+    """Update scripts/nightly.yaml with the version."""
+    script_dir = os.path.dirname(os.path.abspath(__file__))
+    nightly_file = os.path.join(script_dir, 'nightly.yaml')
+    
+    version_parts = version.split('.')
+    if len(version_parts) >= 3:
+        major, minor, patch = version_parts[0], version_parts[1], version_parts[2]
+    else:
+        print(f"Warning: Invalid version format in VERSION.txt: {version}")
+        return
+    
+    try:
+        with open(nightly_file, 'r') as f:
+            content = f.read()
+        
+        # Update Major, Minor, Patch variables
+        content = re.sub(r"(\s+Major:\s*')[^']*('.*)", r"\g<1>" + major + r"\g<2>", content)
+        content = re.sub(r"(\s+Minor:\s*')[^']*('.*)", r"\g<1>" + minor + r"\g<2>", content)
+        content = re.sub(r"(\s+Patch:\s*')[^']*('.*)", r"\g<1>" + patch + r"\g<2>", content)
+        
+        with open(nightly_file, 'w') as f:
+            f.write(content)
+        
+        print(f"Updated nightly.yaml version to {major}.{minor}.{patch}")
+    except IOError as e:
+        print(f"Error updating nightly.yaml: {e}")
+
+def update_release_yml(version):
+    """Update scripts/release.yml with the version."""
+    script_dir = os.path.dirname(os.path.abspath(__file__))
+    release_file = os.path.join(script_dir, 'release.yml')
+    
+    # Extract major.minor.patch from major.minor.patch.tweak
+    version_parts = version.split('.')
+    if len(version_parts) >= 3:
+        release_version = f"{version_parts[0]}.{version_parts[1]}.{version_parts[2]}"
+    else:
+        release_version = version
+    
+    try:
+        with open(release_file, 'r') as f:
+            content = f.read()
+        
+        # Update ReleaseVersion variable
+        content = re.sub(
+            r"(\s+ReleaseVersion:\s*')[^']*('.*)",
+            r"\g<1>" + release_version + r"\g<2>",
+            content
+        )
+        
+        with open(release_file, 'w') as f:
+            f.write(content)
+        
+        print(f"Updated release.yml version to {release_version}")
+    except IOError as e:
+        print(f"Error updating release.yml: {e}")
+
+def main():
+    """Main function."""
+    print("Z3 Version Update Script")
+    print("========================")
+    
+    version = read_version()
+    print(f"Read version from VERSION.txt: {version}")
+    
+    print("\nUpdating files that cannot auto-read VERSION.txt...")
+    
+    update_bazel_module(version)
+    update_nightly_yaml(version)
+    update_release_yml(version)
+    
+    print("\nUpdate complete!")
+    print("\nNote: The following files automatically read from VERSION.txt:")
+    print("  - CMakeLists.txt")
+    print("  - scripts/mk_project.py")
+    print("\nThese do not need manual updates.")
+
+if __name__ == "__main__":
+    main()

src/api/api_solver.cpp

@@ -146,6 +146,8 @@ extern "C" {
         bool proofs_enabled = true, models_enabled = true, unsat_core_enabled = false;
         params_ref p = s->m_params;
         mk_c(c)->params().get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled);
+        if (!s->m_solver_factory)
+            s->m_solver_factory = mk_smt_solver_factory();
         s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic);
         
         param_descrs r;
@@ -274,7 +276,11 @@ extern "C" {
         LOG_Z3_solver_translate(c, s, target);
         RESET_ERROR_CODE();
         params_ref const& p = to_solver(s)->m_params; 
-        Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(target), (solver_factory *)nullptr);
+        solver_factory* translated_factory = nullptr;
+        if (to_solver(s)->m_solver_factory.get()) {
+            translated_factory = to_solver(s)->m_solver_factory->translate(mk_c(target)->m());
+        }
+        Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(target), translated_factory);
         init_solver(c, s);
         sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
         mk_c(target)->save_object(sr);

src/api/python/setup.py

@@ -114,11 +114,11 @@ def _clean_native_build():
 def _z3_version():
     post = os.getenv('Z3_VERSION_SUFFIX', '')
     if RELEASE_DIR is None:
-        fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py')
+        fn = os.path.join(SRC_DIR_REPO, 'VERSION.txt')
         if os.path.exists(fn):
             with open(fn) as f:
                 for line in f:
-                    n = re.match(r".*set_version\((.*), (.*), (.*), (.*)\).*", line)
+                    n = re.match(r"(.*)\.(.*)\.(.*)\.(.*)", line)
                     if not n is None:
                         return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post
         return "?.?.?.?"
@@ -284,7 +284,7 @@ class sdist(_sdist):
 # The Azure Dev Ops pipelines use internal OS version tagging that don't correspond
 # to releases.
 
-internal_build_re = re.compile("(.+)\_7")
+internal_build_re = re.compile("(.+)_7")
 
 class bdist_wheel(_bdist_wheel):
 

src/api/python/z3/z3.py

@@ -653,6 +653,10 @@ class SortRef(AstRef):
         """
         return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
 
+    def __gt__(self, other):
+        """Create the function space Array(self, other)"""
+        return ArraySort(self, other)
+
     def __hash__(self):
         """ Hash code. """
         return AstRef.__hash__(self)

src/ast/euf/euf_ac_plugin.cpp

@@ -686,6 +686,7 @@ namespace euf {
         case eq_status::is_processed_eq:
         case eq_status::is_reducing_eq:
         case eq_status::is_dead_eq:
+        case eq_status::is_passive_eq:
             m_to_simplify_todo.remove(id);
             break;
         case eq_status::is_to_simplify_eq:

src/ast/euf/euf_arith_plugin.cpp

@@ -56,6 +56,32 @@ namespace euf {
         TRACE(plugin, tout << g.bpp(n) << "\n");
         m_add.register_node(n);
         m_mul.register_node(n);
+        expr* e = n->get_expr(), * x, * y;
+        // x - y = x + (* -1 y)
+        if (a.is_sub(e, x, y)) {
+            auto& m = g.get_manager();
+            auto e1 = a.mk_numeral(rational(-1), a.is_int(x));
+            auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr);
+            auto e2 = a.mk_mul(e1, y);
+            enode* es1[2] = { n1, g.find(y)};
+            auto mul = g.find(e2) ? g.find(e2) : g.mk(e2, 0, 2, es1);
+            enode* es2[2] = { g.find(x), mul };
+            expr* e_add = a.mk_add(x, e2);
+            auto add = g.find(e_add) ? g.find(e_add): g.mk(e_add, 0, 2, es2);
+            push_merge(n, add);
+        }
+        // c1 * c2 = c1*c2
+        rational r1, r2;
+        if (a.is_mul(e, x, y) && a.is_numeral(x, r1) && a.is_numeral(y, r2)) {
+            rational r = r1 * r2;
+            auto e1 = a.mk_numeral(r, a.is_int(x));
+            auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr);
+            push_merge(n, n1);
+        }
+        if (a.is_uminus(e, x)) {
+            NOT_IMPLEMENTED_YET();
+        }
+
     }
 
     void arith_plugin::merge_eh(enode* n1, enode* n2) {

src/ast/rewriter/seq_rewriter.cpp

@@ -1450,6 +1450,59 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) {
         result = m_autil.mk_int(0);
         return BR_DONE;
     }
+
+    if (str().is_empty(b)) {
+        result = str().mk_length(a);
+        return BR_DONE;
+    }
+
+    expr_ref_vector as(m()), bs(m());
+    str().get_concat_units(a, as);
+    str().get_concat_units(b, bs);
+
+    auto is_suffix = [&](expr_ref_vector const& as, expr_ref_vector const& bs) {
+        if (as.size() < bs.size())
+            return l_undef;
+        for (unsigned j = 0; j < bs.size(); ++j) {
+            auto a = as.get(as.size() - j - 1);
+            auto b = bs.get(bs.size() - j - 1);
+            if (m().are_equal(a, b))
+                continue;
+            if (m().are_distinct(a, b))
+                return l_false;
+            return l_undef;
+        }
+        return l_true;
+    };
+
+    switch (compare_lengths(as, bs)) {
+    case shorter_c:
+        result = minus_one();
+        return BR_DONE;
+    case same_length_c:
+        result = m().mk_ite(m().mk_eq(a, b), zero(), minus_one());
+        return BR_REWRITE_FULL;
+    case longer_c: {
+        unsigned i = as.size();
+        while (i >= bs.size()) {
+            switch (is_suffix(as, bs)) {
+            case l_undef:
+                return BR_FAILED;
+            case l_true:
+                result = m_autil.mk_sub(str().mk_length(a), m_autil.mk_int(bs.size() - i));
+                return BR_REWRITE3;
+            case l_false:
+                as.pop_back();
+                --i;
+                break;
+            }
+        }
+        break;
+    }
+    default:
+        break;
+    }
+
     return BR_FAILED;
 }
 

src/ast/simplifiers/euf_completion.cpp

@@ -244,7 +244,7 @@ namespace euf {
         unsigned sz = qtail();
         for (unsigned i = qhead(); i < sz; ++i) {
             auto [f, p, d] = m_fmls[i]();
-            if (is_app(f) && to_app(f)->get_num_args() == 1 && symbol("congruences") == to_app(f)->get_decl()->get_name())
+            if (is_congruences(f))
                 map_congruence(to_app(f)->get_arg(0));
         }
     }
@@ -255,6 +255,11 @@ namespace euf {
             return;
         expr_ref_vector args(m);
         expr_mark visited;
+        proof_ref pr(m);
+        expr_dependency_ref dep(m);
+        auto canon = get_canonical(n->get_expr(), pr, dep);
+        args.push_back(canon);
+        visited.mark(canon);
         for (auto s : enode_class(n)) {
             expr_ref r(s->get_expr(), m);
             m_rewriter(r);
@@ -329,6 +334,12 @@ namespace euf {
             if (a->get_root() == b->get_root())
                 return;
 
+            expr_ref x1(x, m);
+            m_rewriter(x1);
+//            enode* a1 = mk_enode(x1);
+//            if (a->get_root() != a1->get_root())
+//                m_egraph.merge(a, a1, nullptr);
+
             TRACE(euf, tout << "merge and propagate\n");
             add_children(a);
             add_children(b);
@@ -344,6 +355,7 @@ namespace euf {
         else if (m.is_not(f, nf)) {
             expr_ref f1(nf, m);
             m_rewriter(f1);
+
             enode* n = mk_enode(f1);
             if (m.is_false(n->get_root()->get_expr()))
                 return;
@@ -351,6 +363,9 @@ namespace euf {
             auto n_false = mk_enode(m.mk_false());
             auto j = to_ptr(push_pr_dep(pr, d));
             m_egraph.merge(n, n_false, j);
+            if (nf != f1) 
+                m_egraph.merge(n, mk_enode(nf), nullptr);
+            
             m_egraph.propagate();
             add_children(n);
             m_should_propagate = true;
@@ -358,7 +373,21 @@ namespace euf {
                 m_side_condition_solver->add_constraint(f, pr, d);
             IF_VERBOSE(1, verbose_stream() << "not: " << nf << "\n");
         }
+        else if (is_congruences(f)) {
+            auto t = to_app(f)->get_arg(0);
+            expr_ref r(t, m);
+            m_rewriter(r);
+            auto a = mk_enode(t);
+            auto b = mk_enode(r);
+            m_egraph.merge(a, b, nullptr);
+            m_egraph.propagate();
+        }
         else {
+            expr_ref f1(f, m);
+            if (!m.is_implies(f) && !is_quantifier(f)) {
+                m_rewriter(f1);
+                f = f1;
+            }
             enode* n = mk_enode(f);
             if (m.is_true(n->get_root()->get_expr()))
                 return;            
@@ -1099,7 +1128,6 @@ namespace euf {
             }
             else
                 UNREACHABLE();
-
         }
         enode* n = m_egraph.find(f);
         if (!n) n = mk_enode(f);
@@ -1108,10 +1136,11 @@ namespace euf {
         d = m.mk_join(d, m_deps.get(r->get_id(), nullptr));
         if (m.proofs_enabled()) {
             pr = prove_eq(n, r);
-            if (get_canonical_proof(r)) 
-                pr = m.mk_transitivity(pr, get_canonical_proof(r));            
+            if (get_canonical_proof(r))
+                pr = m.mk_transitivity(pr, get_canonical_proof(r));
         }
-        SASSERT(m_canonical.get(r->get_id()));
+        if (!m_canonical.get(r->get_id()))
+            m_canonical.setx(r->get_id(), r->get_expr());
         return expr_ref(m_canonical.get(r->get_id()), m);
     }
 

src/ast/simplifiers/euf_completion.h

@@ -175,6 +175,10 @@ namespace euf {
         void map_congruence(expr* t);
         void add_consequence(expr* t);
 
+        bool is_congruences(expr* f) const {
+            return is_app(f) && to_app(f)->get_num_args() == 1 && symbol("congruences") == to_app(f)->get_decl()->get_name();
+        }
+
         // Enable equality propagation inside of quantifiers
         // add quantifier bodies as closure terms to the E-graph.
         // use fresh variables for bound variables, but such that the fresh variables are 

src/ast/simplifiers/extract_eqs.cpp

@@ -115,7 +115,7 @@ namespace euf {
                 if (is_eq_of(x2, y1, z, s, t) && is_complementary(x1, y2))
                     eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(x1, s, t), m), d));
             }
-            if (m.is_and(f, x1, y1) && m.is_or(x, x1, x2) && m.is_or(y1, y1, y2)) {
+            if (m.is_and(f, x1, y1) && m.is_or(x1, x1, x2) && m.is_or(y1, y1, y2)) {
                 expr* z = nullptr, *t = nullptr, *s = nullptr;
                 if (is_eq_of(x1, y1, z, s, t) && is_complementary(x2, y2)) 
                     eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(y2, s, t), m), d));

src/ast/simplifiers/model_reconstruction_trail.cpp

@@ -80,6 +80,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
                 add_vars(v, free_vars);
                 st.add(dependent_expr(m, m.mk_eq(k, v), nullptr, nullptr));
             }
+            m_trail_stack.push(value_trail(t->m_active));
             t->m_active = false;
             continue;
         }
@@ -90,6 +91,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
                 TRACE(simplifier, tout << "replay removed " << r << "\n");
                 st.add(r);
             }
+            m_trail_stack.push(value_trail(t->m_active));
             t->m_active = false;
             continue;
         }

src/math/lp/lar_solver.cpp

@@ -1523,7 +1523,7 @@ namespace lp {
         if (!m_imp->m_columns_with_changed_bounds.empty())
             return false;
 
-        m_imp->m_delta = get_core_solver().find_delta_for_strict_bounds(mpq(1));
+        m_imp->m_delta = get_core_solver().find_delta_for_strict_bounds(m_imp->m_settings.m_epsilon);
         unsigned j;
         unsigned n = get_core_solver().r_x().size();
         do {
@@ -1545,7 +1545,7 @@ namespace lp {
     }
 
     void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map<lpvar, mpq>& variable_values) const {
-        mpq delta = get_core_solver().find_delta_for_strict_bounds(mpq(1));
+        mpq delta = get_core_solver().find_delta_for_strict_bounds(m_imp->m_settings.m_epsilon);
         for (unsigned i = 0; i < get_core_solver().r_x().size(); i++) {
             const impq& rp = get_core_solver().r_x(i);
             variable_values[i] = rp.x + delta * rp.y;
@@ -1569,7 +1569,7 @@ namespace lp {
         }
         if (y_is_zero)
             return;
-        mpq delta = get_core_solver().find_delta_for_strict_bounds(mpq(1));
+        mpq delta = get_core_solver().find_delta_for_strict_bounds(m_imp->m_settings.m_epsilon);
         for (unsigned j = 0; j < number_of_vars(); j++) {
             auto& v = get_core_solver().r_x(j);
             if (!v.y.is_zero()) {

src/math/lp/lp_settings.cpp

@@ -34,6 +34,8 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
     report_frequency = p.arith_rep_freq();
     m_simplex_strategy = static_cast<lp::simplex_strategy_enum>(p.arith_simplex_strategy());
     m_nlsat_delay = p.arith_nl_delay();
+    auto eps = p.arith_epsilon();
+    m_epsilon = rational(std::max(1, (int)(100000*eps)), 100000); 
     m_dio = lp_p.dio();
     m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory();
     m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf();

src/math/lp/lp_settings.h

@@ -245,6 +245,7 @@ private:
 public:
     unsigned         limit_on_rows_for_hnf_cutter = 75;
     unsigned         limit_on_columns_for_hnf_cutter = 150;
+    mpq              m_epsilon = mpq(1);
 private:
     unsigned         m_nlsat_delay = 0;
     bool             m_enable_hnf = true;

src/model/model_smt2_pp.cpp

@@ -42,8 +42,13 @@ static unsigned pp_symbol(std::ostream & out, symbol const & s) {
         return static_cast<unsigned>(str.length());
     }
     else {
-        out << s.bare_str();
-        return static_cast<unsigned>(strlen(s.bare_str()));
+        if (s.is_null()) {
+            out << "null";
+            return 4; // length of "null"
+        } else {
+            out << s.bare_str();
+            return static_cast<unsigned>(strlen(s.bare_str()));
+        }
     }
 }
 

src/nlsat/nlsat_explain.cpp

@@ -618,22 +618,55 @@ namespace nlsat {
             }
         }
 
-	// For each p in ps add the leading coefficent to the projection,
-        void add_lc(polynomial_ref_vector &ps, var x) {
+// The monomials have to be square free according to
+//"An improved projection operation for cylindrical algebraic decomposition of three-dimensional space", by McCallum, Scott
+            
+        bool is_square_free(polynomial_ref_vector &ps, var x) {
+            polynomial_ref p(m_pm);
+            polynomial_ref lc_poly(m_pm);
+            polynomial_ref disc_poly(m_pm); 
+
+            for (unsigned i = 0; i < ps.size(); i++) {
+                p = ps.get(i);
+                unsigned k_deg = m_pm.degree(p, x); 
+                if (k_deg == 0)
+                    continue;
+                // p depends on x
+                disc_poly = discriminant(p, x); // Use global helper
+                if (sign(disc_poly) == 0) { // Discriminant is zero
+                    TRACE(nlsat_explain, tout << "p is not square free:\n ";
+                          display(tout, p); tout << "\ndiscriminant: "; display(tout, disc_poly) << "\n";
+                          m_solver.display_assignment(tout) << '\n';
+                          m_solver.display_var(tout << "x:", x) << '\n';
+                        );
+
+                    return false;
+                }
+            }
+            return true;
+        }
+        
+     	// If each p from ps is square-free then add the leading coefficents to the projection. 
+	// Otherwise, add each coefficient of each p to the projection.
+        void add_lcs(polynomial_ref_vector &ps, var x) {
             polynomial_ref p(m_pm);
             polynomial_ref coeff(m_pm);
 
-            // Add coefficients based on well-orientedness
+            bool sqf = is_square_free(ps, x);
+            // Add the leading or all coeffs, depening on being square-free
             for (unsigned i = 0; i < ps.size(); i++) {
                 p = ps.get(i);
                 unsigned k_deg = m_pm.degree(p, x);
                 if (k_deg == 0) continue;
                 // p depends on x
                 TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p) << "\n";);
-                coeff = m_pm.coeff(p, x, k_deg);
-                TRACE(nlsat_explain, tout << "    coeff deg " << k_deg << ": "; display(tout, coeff) << "\n";);
-                insert_fresh_factors_in_todo(coeff);
-                
+                for (unsigned j_coeff_deg = k_deg; j_coeff_deg >= 1; j_coeff_deg--) { 
+                    coeff = m_pm.coeff(p, x, j_coeff_deg);
+                    TRACE(nlsat_explain, tout << "    coeff deg " << j_coeff_deg << ": "; display(tout, coeff) << "\n";);
+                    insert_fresh_factors_in_todo(coeff);
+                    if (sqf)
+                        break;
+                }
             }
         }
 
@@ -1175,7 +1208,7 @@ namespace nlsat {
                 TRACE(nlsat_explain,  tout << "project loop, processing var "; display_var(tout, x);
                       tout << "\npolynomials\n";
                       display(tout, ps); tout << "\n";);
-                add_lc(ps, x);
+                add_lcs(ps, x);
                 psc_discriminant(ps, x);
                 psc_resultant(ps, x);
                 if (m_todo.empty())
@@ -1223,7 +1256,7 @@ namespace nlsat {
                 }
                 TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
                       display(tout, ps); tout << "\n";);
-                add_lc(ps, x);
+                add_lcs(ps, x);
                 psc_discriminant(ps, x);
                 psc_resultant(ps, x);
                 

src/params/smt_params_helper.pyg

@@ -86,6 +86,7 @@ def_module_params(module_name='smt',
 			  ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
 			  ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),
                           ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
+			  ('arith.epsilon', DOUBLE, 1.0, 'initial value of epsilon used for model generation of infinitesimals'),
                           ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
                           ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
                           ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),

src/params/theory_arith_params.cpp

@@ -41,6 +41,8 @@ void theory_arith_params::updt_params(params_ref const & _p) {
     m_nl_arith_propagate_linear_monomials = p.arith_nl_propagate_linear_monomials();
     m_nl_arith_optimize_bounds = p.arith_nl_optimize_bounds();
     m_nl_arith_cross_nested = p.arith_nl_cross_nested();
+    auto eps = p.arith_epsilon();
+    m_arith_epsilon = rational(std::max(1, (int)(100000*eps)), 100000); 
 
     arith_rewriter_params ap(_p);
     m_arith_eq2ineq = ap.eq2ineq();
@@ -99,4 +101,5 @@ void theory_arith_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_nl_arith_cross_nested);
     DISPLAY_PARAM(m_arith_validate);
     DISPLAY_PARAM(m_arith_dump_lemmas);
+    DISPLAY_PARAM(m_arith_epsilon);
 }

src/params/theory_arith_params.h

@@ -20,6 +20,7 @@ Revision History:
 
 #include<climits>
 #include "util/params.h"
+#include "util/rational.h"
 
 enum class arith_solver_id {
     AS_NO_ARITH,              // 0
@@ -76,6 +77,7 @@ struct theory_arith_params {
     unsigned                m_arith_branch_cut_ratio = 2;
     bool                    m_arith_int_eq_branching = false;
     bool                    m_arith_enum_const_mod = false;
+    rational                m_arith_epsilon = rational::one();
 
     bool                    m_arith_gcd_test = true;
     bool                    m_arith_eager_gcd = false;

src/sat/smt/arith_axioms.cpp

@@ -168,6 +168,9 @@ namespace arith {
             add_clause(eqz, mod_ge_0);
             add_clause(eqz, mod_lt_q);
 
+            if (!a.is_uminus(q))
+                add_clause(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_uminus(q)))));
+
 #if 0
             /*literal div_ge_0   = */ mk_literal(a.mk_ge(div, zero));
             /*literal div_le_0   = */ mk_literal(a.mk_le(div, zero));

src/smt/smt_solver.cpp

@@ -527,6 +527,10 @@ public:
     solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override {
         return mk_smt_solver(m, p, logic);
     }
+    
+    solver_factory* translate(ast_manager& m) override {
+        return alloc(smt_solver_factory);
+    }
 };
 }
 

src/smt/theory_arith_core.h

@@ -3174,7 +3174,8 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::compute_epsilon() {
-        m_epsilon = numeral(1);
+        auto eps = ctx.get_fparams().m_arith_epsilon;        
+        m_epsilon = numeral(eps);
         theory_var num = get_num_vars();
         for (theory_var v = 0; v < num; v++) {
             bound * l = lower(v);

src/smt/theory_lra.cpp

@@ -1296,10 +1296,14 @@ public:
             // q = 0 or p = (p mod q) + q * (p div q)
             // q = 0 or (p mod q) >= 0
             // q = 0 or (p mod q) < abs(q)
+            // q >= 0 or (p mod q) = (p mod -q)
             
             mk_axiom(eqz, eq);
             mk_axiom(eqz, mod_ge_0);
             mk_axiom(eqz, mod_lt_q);
+            if (!a.is_uminus(q)) 
+                mk_axiom(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_uminus(q)))));
+            
             m_arith_eq_adapter.mk_axioms(th.ensure_enode(mod_r), th.ensure_enode(p));
 
             if (a.is_zero(p)) {
@@ -3734,6 +3738,8 @@ public:
         unsigned_vector vars;
         unsigned j = 0;
         for (auto [e, t, g] : solutions) {
+            if (!ctx().e_internalized(e))
+                continue;
             auto n = get_enode(e);
             if (!n) {
                 solutions[j++] = { e, t, g };

src/solver/combined_solver.cpp

@@ -424,6 +424,12 @@ public:
                                   (*m_f2)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic),
                                   p);
     }
+    
+    solver_factory* translate(ast_manager& m) override {
+        solver_factory* translated_f1 = m_f1->translate(m);
+        solver_factory* translated_f2 = m_f2->translate(m);
+        return alloc(combined_solver_factory, translated_f1, translated_f2);
+    }
 };
 
 solver_factory * mk_combined_solver_factory(solver_factory * f1, solver_factory * f2) {

src/solver/solver.h

@@ -32,6 +32,11 @@ class solver_factory {
 public:
     virtual ~solver_factory() = default;
     virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) = 0;
+    /**
+       \brief Create a clone of the solver factory for the given ast_manager.
+       The clone should be functionally equivalent but associated with the target manager.
+    */
+    virtual solver_factory* translate(ast_manager& m) = 0;
 };
 
 solver_factory * mk_smt_strategic_solver_factory(symbol const & logic = symbol::null);

src/solver/tactic2solver.cpp

@@ -390,6 +390,11 @@ public:
     solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override {
         return mk_tactic2solver(m, m_tactic.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, logic);
     }
+    
+    solver_factory* translate(ast_manager& m) override {
+        tactic* translated_tactic = m_tactic->translate(m);
+        return alloc(tactic2solver_factory, translated_tactic);
+    }
 };
 
 class tactic_factory2solver_factory : public solver_factory {
@@ -402,6 +407,10 @@ public:
         tactic * t = (*m_factory)(m, p);
         return mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic);
     }
+    
+    solver_factory* translate(ast_manager& m) override {
+        return alloc(tactic_factory2solver_factory, m_factory);
+    }
 };
 }
 

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -60,6 +60,10 @@ public:
         auto s = mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic);
         return s;
     }
+    
+    solver_factory* translate(ast_manager& m) override {
+        return alloc(smt_nested_solver_factory);
+    }
 };
 
 tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) {
@@ -185,6 +189,10 @@ public:
                                   mk_solver_for_logic(m, p, l), 
                                   p);
     }
+    
+    solver_factory* translate(ast_manager& m) override {
+        return alloc(smt_strategic_solver_factory, m_logic);
+    }
 };
 
 solver_factory * mk_smt_strategic_solver_factory(symbol const & logic) {