mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

Merge 8e8799dbd3 into 87d1131620

Browse source
This commit is contained in:
Don Syme 2025-10-30 12:01:47 +01:00 • committed by GitHub
commit b626cfb07c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
7 changed files with 803 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

140
.github/ISSUE_TEMPLATE/01-bug-report.yml vendored Normal file
View file

@ -0,0 +1,140 @@
name: 🐛 Bug Report
description: Report a bug or incorrect behavior in Z3
title: "[Bug] "
labels: ["bug"]
body:
- type: markdown
attributes:
value: |
Thank you for reporting a bug! This helps make Z3 better.
Please provide as much detail as possible to help us reproduce and fix the issue.
- type: dropdown
id: bug-category
attributes:
label: Bug Category
description: What type of bug are you experiencing?
options:
- Crash/Assertion failure
- Incorrect result (SAT/UNSAT/Unknown)
- Performance regression
- Memory issue/leak
- API behavior
- Build/Installation issue
- Other
validations:
required: true
- type: textarea
id: description
attributes:
label: Bug Description
description: A clear and concise description of the bug
placeholder: Describe what happens vs what you expected...
validations:
required: true
- type: textarea
id: minimal-example
attributes:
label: Minimal Reproduction
description: Please provide the smallest possible example that reproduces the issue
placeholder: |
(set-logic QF_LIA)
(declare-fun x () Int)
(assert (> x 5))
(check-sat)
render: smt2
validations:
required: true
- type: textarea
id: expected-behavior
attributes:
label: Expected Behavior
description: What did you expect to happen?
validations:
required: true
- type: textarea
id: actual-behavior
attributes:
label: Actual Behavior
description: What actually happened? Include full error messages/output
validations:
required: true
- type: input
id: version
attributes:
label: Z3 Version
description: What version of Z3 are you using? (run `z3 --version`)
placeholder: Z3 version 4.13.0 - 64 bit
validations:
required: true
- type: dropdown
id: platform
attributes:
label: Platform
description: What platform are you running Z3 on?
options:
- Linux x86_64
- macOS ARM64 (Apple Silicon)
- macOS Intel x86_64
- Windows x86_64
- Windows ARM64
- Other (specify in additional context)
validations:
required: true
- type: dropdown
id: interface
attributes:
label: Interface Used
description: How are you using Z3?
options:
- Command line (z3 executable)
- Python API
- C++ API
- C API
- Java API
- .NET API
- OCaml API
- JavaScript/WASM API
- Other (specify below)
validations:
required: true
- type: textarea
id: installation-method
attributes:
label: Installation Method
description: How did you install Z3?
placeholder: "e.g., pip install z3-solver, built from source, downloaded from releases, package manager, etc."
- type: textarea
id: additional-context
attributes:
label: Additional Context
description: Any other information that might be helpful (stack traces, related issues, workarounds, etc.)
- type: checkboxes
id: regression
attributes:
label: Regression Check
description: Help us identify if this is a recent regression
options:
- label: This worked in a previous version of Z3
required: false
- label: I can provide the last working version
required: false
- type: markdown
attributes:
value: |
### Before submitting
- [ ] I searched existing issues and couldn't find a duplicate
- [ ] I provided a minimal reproduction case
- [ ] I included the Z3 version and platform information

163
.github/ISSUE_TEMPLATE/02-performance-issue.yml vendored Normal file
View file

@ -0,0 +1,163 @@
name: ⚡ Performance Issue
description: Report performance problems or regressions in Z3
title: "[Performance] "
labels: ["performance"]
body:
- type: markdown
attributes:
value: |
Thank you for reporting a performance issue! This helps us keep Z3 fast and efficient.
- type: dropdown
id: performance-type
attributes:
label: Performance Issue Type
description: What kind of performance problem are you experiencing?
options:
- Slow solving (takes too long)
- Memory usage (uses too much memory)
- Timeout/infinite loop
- Regression (was faster in previous version)
- Scalability issue (doesn't scale well)
validations:
required: true
- type: textarea
id: description
attributes:
label: Issue Description
description: Describe the performance problem
placeholder: Z3 takes much longer than expected to solve this formula...
validations:
required: true
- type: textarea
id: formula
attributes:
label: Input Formula
description: Please provide the formula that exhibits the performance issue. For large files, consider attaching or linking to them.
placeholder: |
(set-logic QF_BV)
(declare-fun x () (_ BitVec 32))
; ... large formula here
render: smt2
validations:
required: true
- type: textarea
id: timing-info
attributes:
label: Performance Measurements
description: Provide timing and memory usage information
placeholder: |
Current behavior: Takes 300+ seconds, uses 8GB memory
Expected: Should complete in <10 seconds based on similar formulas
Command used: z3 -smt2 formula.smt2
System specs: Intel i7, 16GB RAM
value: |
**Current performance:**
- Time:
- Memory:
- Command:
**Expected performance:**
-
**System specifications:**
- CPU:
- Memory:
- Other relevant specs:
validations:
required: true
- type: input
id: version
attributes:
label: Z3 Version
description: What version of Z3 are you using?
placeholder: Z3 version 4.13.0 - 64 bit
validations:
required: true
- type: dropdown
id: regression-info
attributes:
label: Is this a regression?
description: Did this work better in a previous version?
options:
- "No, this has always been slow"
- "Yes, this is slower than a previous version"
- "I don't know"
validations:
required: true
- type: input
id: last-working-version
attributes:
label: Last Working Version (if regression)
description: If this is a regression, what was the last version that performed well?
placeholder: e.g., Z3 4.12.6
- type: dropdown
id: theory
attributes:
label: Primary Theory
description: What's the main theory used in your formula?
options:
- Linear Arithmetic (LIA/LRA)
- Bit-vectors (QF_BV)
- Arrays
- Strings
- Uninterpreted Functions
- Quantifiers
- Mixed/Multiple theories
- Other/Unknown
validations:
required: true
- type: textarea
id: solver-options
attributes:
label: Solver Configuration
description: Are you using any specific solver options or tactics?
placeholder: |
Command line: z3 -smt2 -T:300 formula.smt2
Options: sat.max_memory=4096
Tactics: None / Custom tactic used
- type: textarea
id: workarounds
attributes:
label: Workarounds Found
description: Have you found any parameter changes or tactics that improve performance?
placeholder: Setting rewriter.bv_sort_ac=true helps significantly
- type: textarea
id: additional-context
attributes:
label: Additional Context
description: Any other details that might help (related formulas, use case, etc.)
- type: checkboxes
id: testing
attributes:
label: Testing Information
description: Help us understand your testing approach
options:
- label: I tested with the latest Z3 version
required: false
- label: I can provide the input file separately if it's too large
required: false
- label: This is blocking my work/research
required: false
- type: markdown
attributes:
value: |
### Before submitting
- [ ] I searched existing performance issues
- [ ] I provided timing/memory measurements
- [ ] I specified the Z3 version and system specs
For very large input files, consider uploading them separately or providing a link.

147
.github/ISSUE_TEMPLATE/03-feature-request.yml vendored Normal file
View file

@ -0,0 +1,147 @@
name: ✨ Feature Request
description: Suggest a new feature or enhancement for Z3
title: "[Feature] "
labels: ["enhancement"]
body:
- type: markdown
attributes:
value: |
Thank you for suggesting a new feature! This helps us understand what users need.
- type: dropdown
id: feature-category
attributes:
label: Feature Category
description: What area does this feature request relate to?
options:
- New theory support
- API enhancement (Python/C++/Java/.NET/etc.)
- Solver tactics/strategies
- SMT-LIB2 standard compliance
- Build system/packaging
- Performance optimization
- Documentation
- Developer tools/workflow
- Other
validations:
required: true
- type: textarea
id: summary
attributes:
label: Feature Summary
description: A clear and concise description of the feature you'd like to see
placeholder: I would like Z3 to support...
validations:
required: true
- type: textarea
id: motivation
attributes:
label: Motivation and Use Case
description: Why do you need this feature? What problem does it solve?
placeholder: |
This feature would help with...
My use case is...
Currently, I have to work around this by...
validations:
required: true
- type: textarea
id: proposed-solution
attributes:
label: Proposed Solution
description: How do you envision this feature working?
placeholder: |
I think this could be implemented by...
The API could look like...
An example usage would be...
- type: textarea
id: example
attributes:
label: Example Usage
description: Show how you would use this feature (code examples, SMT-LIB2 syntax, etc.)
placeholder: |
// Python API example:
solver.set_option("new_feature", True)
; SMT-LIB2 example:
(set-option :new-feature true)
(assert ...)
render: python
- type: textarea
id: alternatives
attributes:
label: Alternatives Considered
description: Have you considered any alternative solutions or workarounds?
placeholder: |
I tried using... but it doesn't work because...
Another approach would be... but it has the drawback of...
- type: dropdown
id: priority
attributes:
label: Priority
description: How important is this feature for your work?
options:
- Low - Nice to have
- Medium - Would be helpful
- High - Important for my work
- Critical - Blocking my research/project
validations:
required: true
- type: dropdown
id: implementation-help
attributes:
label: Implementation Help
description: Would you be willing to help implement this feature?
options:
- I would like to implement this myself
- I could help with implementation if guided
- I can help with testing/feedback
- I can only provide requirements/feedback
validations:
required: true
- type: textarea
id: related-work
attributes:
label: Related Work
description: Are there similar features in other solvers, research papers, or standards?
placeholder: |
Similar to CVC5's feature...
Described in paper: ...
SMT-LIB2 standard section: ...
- type: checkboxes
id: compatibility
attributes:
label: Compatibility Considerations
description: Please consider compatibility aspects
options:
- label: This feature should maintain backward compatibility
required: false
- label: This feature might require breaking API changes
required: false
- label: This feature affects SMT-LIB2 compliance
required: false
- type: textarea
id: additional-context
attributes:
label: Additional Context
description: Any other information that might be helpful (screenshots, links, research papers, etc.)
- type: markdown
attributes:
value: |
### Before submitting
- [ ] I searched existing feature requests and issues
- [ ] I provided clear motivation and use cases
- [ ] I considered backward compatibility implications
### After submitting
Community discussion and maintainer feedback will help refine this feature request. Complex features may require design discussions before implementation begins.

111
.github/ISSUE_TEMPLATE/04-question.yml vendored Normal file
View file

@ -0,0 +1,111 @@
name: ❓ Question
description: Ask a question about using Z3 or understanding its behavior
title: "[Question] "
labels: ["question"]
body:
- type: markdown
attributes:
value: |
### ⚠️ Before asking a question
For general Z3 usage questions, tutorials, and discussions, please consider using:
- **[GitHub Discussions](../../discussions)** - Best for open-ended discussions
- **[Stack Overflow](https://stackoverflow.com/questions/tagged/z3)** - Great for specific coding questions
- **[Z3 Guide](https://microsoft.github.io/z3guide/)** - Comprehensive tutorials and documentation
Use this issue template only for questions that are:
- Specific to Z3's internal behavior or design decisions
- Related to undocumented behavior that might be a bug
- Questions that could lead to documentation improvements
- type: dropdown
id: question-type
attributes:
label: Question Type
description: What kind of question is this?
options:
- Usage/API question
- Behavior clarification
- Theory/algorithm question
- Build/installation question
- Documentation gap
- Design/architectural question
validations:
required: true
- type: textarea
id: question
attributes:
label: Question
description: What would you like to know?
placeholder: I'm trying to understand why Z3 behaves differently when...
validations:
required: true
- type: textarea
id: context
attributes:
label: Context
description: Provide relevant background about what you're trying to achieve
placeholder: |
I'm working on...
My goal is to...
I expected... but saw...
- type: textarea
id: example
attributes:
label: Example (if applicable)
description: If relevant, provide a minimal example that illustrates your question
placeholder: |
(set-logic QF_LIA)
(declare-fun x () Int)
(assert (> x 0))
(check-sat)
; Why does this return sat instead of unsat?
render: smt2
- type: input
id: version
attributes:
label: Z3 Version
description: What version are you using?
placeholder: Z3 version 4.13.0 - 64 bit
- type: textarea
id: research-done
attributes:
label: Research Done
description: What have you already tried or looked at?
placeholder: |
I checked the documentation at...
I searched for similar questions and found...
I tried using the following approaches...
- type: checkboxes
id: question-check
attributes:
label: Question Guidelines
description: Please confirm
options:
- label: This is specific to Z3's behavior/design and not a general SMT question
required: true
- label: I searched existing issues and discussions for similar questions
required: true
- label: I considered whether Stack Overflow or GitHub Discussions might be more appropriate
required: true
- type: markdown
attributes:
value: |
### Alternative places for questions:
- 💬 **[GitHub Discussions](../../discussions)** - For open-ended discussions about Z3 usage, best practices, and community Q&A
- 📚 **[Stack Overflow (z3 tag)](https://stackoverflow.com/questions/tagged/z3)** - For specific programming questions with Z3 APIs
- 📖 **[Z3 Guide](https://microsoft.github.io/z3guide/)** - For tutorials and comprehensive documentation
- 📝 **[Z3 API Documentation](https://z3prover.github.io/api/html/index.html)** - For API reference
Questions asked here should ideally lead to:
- Documentation improvements
- Bug reports (if the behavior is unexpected)
- Feature requests (if functionality is missing)

160
.github/ISSUE_TEMPLATE/05-build-installation.yml vendored Normal file
View file

@ -0,0 +1,160 @@
name: 🔧 Build/Installation Issue
description: Report problems with building or installing Z3
title: "[Build] "
labels: ["build/release"]
body:
- type: markdown
attributes:
value: |
Thank you for reporting a build or installation issue!
- type: dropdown
id: build-type
attributes:
label: Build/Installation Method
description: How are you trying to build or install Z3?
options:
- Building from source (CMake)
- Building from source (Python scripts)
- pip install z3-solver
- Package manager (apt, brew, vcpkg, etc.)
- Pre-built binaries from releases
- Building language bindings (Java, .NET, OCaml)
- Other
validations:
required: true
- type: dropdown
id: platform
attributes:
label: Platform
description: What platform are you building on?
options:
- Linux (Ubuntu/Debian)
- Linux (RedHat/CentOS/Fedora)
- Linux (other distribution)
- macOS (Intel)
- macOS (Apple Silicon)
- Windows (MSVC)
- Windows (MinGW/MSYS2)
- Windows (Cygwin)
- Other Unix-like system
- Other
validations:
required: true
- type: textarea
id: description
attributes:
label: Issue Description
description: Describe what went wrong during build/installation
placeholder: The build fails with error... / Installation doesn't work because...
validations:
required: true
- type: textarea
id: build-commands
attributes:
label: Build Commands
description: Show the exact commands you used
placeholder: |
mkdir build
cd build
cmake ..
make
render: bash
validations:
required: true
- type: textarea
id: error-output
attributes:
label: Error Output
description: Paste the complete error message or build failure output
placeholder: |
-- Configuring done
CMake Error: ...
make: *** [target] Error 1
render: text
validations:
required: true
- type: textarea
id: system-info
attributes:
label: System Information
description: Provide details about your build environment
placeholder: |
OS: Ubuntu 22.04
Compiler: gcc 11.4.0
CMake: 3.22.1
Python: 3.10.12
Java: OpenJDK 11.0.16 (if building Java bindings)
value: |
**Operating System:**
**Compiler:**
**CMake version:**
**Python version:**
**Other relevant tools:**
validations:
required: true
- type: textarea
id: cmake-options
attributes:
label: CMake Configuration (if applicable)
description: What CMake options or configuration did you use?
placeholder: |
cmake -DCMAKE_BUILD_TYPE=Release -DZ3_BUILD_PYTHON_BINDINGS=ON ..
render: bash
- type: textarea
id: dependencies
attributes:
label: Dependencies
description: What dependencies do you have installed? Any missing?
placeholder: |
Installed: build-essential, cmake, python3-dev
Missing: Not sure what's missing
- type: textarea
id: workarounds
attributes:
label: Workarounds Tried
description: What have you tried to fix this issue?
placeholder: |
- Tried different CMake options
- Reinstalled dependencies
- Checked similar issues
- type: checkboxes
id: build-info
attributes:
label: Additional Information
description: Help us understand your build environment
options:
- label: This worked in a previous version of Z3
required: false
- label: This is a fresh/clean build (not incremental)
required: false
- label: I can provide more detailed logs if needed
required: false
- type: textarea
id: additional-context
attributes:
label: Additional Context
description: Any other relevant information (Docker, CI environment, cross-compilation, etc.)
- type: markdown
attributes:
value: |
### Before submitting
- [ ] I searched existing build-related issues
- [ ] I provided the complete error output
- [ ] I included my system/environment details
### Common build documentation:
- [CMake build instructions](https://github.com/Z3Prover/z3/blob/master/README-CMake.md)
- [Main README](https://github.com/Z3Prover/z3/blob/master/README.md)
- [Python API installation](https://pypi.org/project/z3-solver/)

65
.github/ISSUE_TEMPLATE/06-other.yml vendored Normal file
View file

@ -0,0 +1,65 @@
name: 📋 Other Issue
description: For issues that don't fit other categories
title: "[Other] "
labels: []
body:
- type: markdown
attributes:
value: |
Please use this template only if your issue doesn't fit any of the other specific categories.
Consider whether your issue might be:
- **Bug Report** - Z3 crashes, gives wrong results, or behaves unexpectedly
- **Performance Issue** - Z3 is slower than expected or uses too much memory
- **Feature Request** - You need functionality that doesn't exist yet
- **Build/Installation** - Problems compiling or installing Z3
- **Question** - You need help understanding Z3's behavior
- type: dropdown
id: issue-category
attributes:
label: Issue Category
description: What type of issue is this?
options:
- Documentation problem
- Website/repository maintenance
- Security concern
- License question
- Community/governance
- CI/Testing infrastructure
- Release process
- Other (please specify)
validations:
required: true
- type: textarea
id: description
attributes:
label: Description
description: Please describe your issue in detail
validations:
required: true
- type: textarea
id: context
attributes:
label: Context
description: Additional context that might be helpful
placeholder: |
Related documentation:
Affected pages/sections:
Relevant links:
- type: textarea
id: proposed-solution
attributes:
label: Proposed Solution (if any)
description: If you have ideas on how to address this issue
- type: markdown
attributes:
value: |
### Before submitting
- [ ] I confirmed this doesn't fit other issue categories
- [ ] I searched for existing similar issues
- [ ] I provided sufficient detail for maintainers to understand the issue

17
.github/ISSUE_TEMPLATE/config.yml vendored Normal file
View file

@ -0,0 +1,17 @@
blank_issues_enabled: false
contact_links:
- name: 💬 GitHub Discussions
url: https://github.com/Z3Prover/z3/discussions
about: For general questions, usage help, and community discussions
- name: 📚 Stack Overflow
url: https://stackoverflow.com/questions/tagged/z3
about: For specific programming questions and code examples with Z3 APIs
- name: 📖 Z3 Guide
url: https://microsoft.github.io/z3guide/
about: Comprehensive tutorials and documentation for learning Z3
- name: 📝 API Documentation
url: https://z3prover.github.io/api/html/index.html
about: Complete API reference for all Z3 language bindings
- name: 🔬 Z3 Theory and Research
url: https://theory.stanford.edu/~nikolaj/programmingz3.html
about: Academic resources and theory behind Z3's algorithms