mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 03:32:28 +00:00
Merge 8e8799dbd3 into efd5d04af5
This commit is contained in:
Don Syme
GitHub
commit
7ff64fdd2f
7 changed files with 803 additions and 0 deletions
140
.github/ISSUE_TEMPLATE/01-bug-report.yml
vendored
Normal file
140
.github/ISSUE_TEMPLATE/01-bug-report.yml
vendored
Normal 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
163
.github/ISSUE_TEMPLATE/02-performance-issue.yml
vendored
Normal 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
147
.github/ISSUE_TEMPLATE/03-feature-request.yml
vendored
Normal 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
111
.github/ISSUE_TEMPLATE/04-question.yml
vendored
Normal 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
160
.github/ISSUE_TEMPLATE/05-build-installation.yml
vendored
Normal 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
65
.github/ISSUE_TEMPLATE/06-other.yml
vendored
Normal 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
17
.github/ISSUE_TEMPLATE/config.yml
vendored
Normal 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
|
||||||
Loading…
Add table
Add a link
Reference in a new issue