Daily Backlog Burner: Add comprehensive issue templates for improved triage

.github/ISSUE_TEMPLATE/01-bug-report.yml

@@ -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

.github/ISSUE_TEMPLATE/02-performance-issue.yml

@@ -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.