Skip to content

Issues: GaloisInc/what4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

39 Open 69 Closed
39 Open 69 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

What4 over-eagerly produces counterexamples with ArrayMapping instead of ArrayConcrete bug Something isn't working
#271 opened Sep 11, 2024 by RyanGlScott
Improve documentation for WordMap documentation Improvements or additions to documentation
#267 opened Jun 5, 2024 by langston-barrett
Concretization enhancement New feature or request
#259 opened Apr 17, 2024 by langston-barrett
1
@langston-barrett
2
Document Builder expression simplifications
#253 opened Jan 18, 2024 by andreistefanescu
Add support for general sum types enhancement New feature or request
#251 opened Jan 15, 2024 by RyanGlScott
Tests for the preservation of abstract values
#249 opened Dec 6, 2023 by langston-barrett
Abstract values are not preserved by certain calls to bvAdd bug Something isn't working
#248 opened Dec 6, 2023 by langston-barrett
3
Do {Nonce,}AppExprs need annotations?
#246 opened Dec 6, 2023 by langston-barrett
1
Use What4.Serialize.Parser to parse solver models/values.
#228 opened Dec 20, 2022 by andreistefanescu
@andreistefanescu
1
Incorrect documentation for little-endian functions in What4.SWord documentation Improvements or additions to documentation
#225 opened Dec 5, 2022 by RyanGlScott
Test problematic SMT formulas from Cryptol's negshift test case CI Issues related to continuous integration
#223 opened Nov 21, 2022 by RyanGlScott
Support SMT-LIB's str.to_code and str.from_code functions over strings enhancement New feature or request
#222 opened Nov 21, 2022 by RyanGlScott
Try splitting up What4.Expr.Builder to improve compile times enhancement New feature or request performance Issues related to compile-time or runtime performance
#220 opened Oct 14, 2022 by RyanGlScott
Add inNewFrame2 enhancement New feature or request
#218 opened Sep 8, 2022 by RyanGlScott
cvc5 is too fast for challenge problem in timeout test bug Something isn't working
#210 opened Jul 1, 2022 by arjunvish
Problem feature lists for SMT solvers are not up to date enhancement New feature or request
#209 opened Jul 1, 2022 by arjunvish
"early unsat" bookeeping error bug Something isn't working
#196 opened Apr 1, 2022 by robdockins
Reconsider absorption rules for boolean predicates tech-debt
#194 opened Mar 11, 2022 by robdockins
Add support for Z3 minimization/maximization enhancement New feature or request
#188 opened Feb 17, 2022 by RyanGlScott
"float reduce" setting is inaccesssable tech-debt
#178 opened Jan 11, 2022 by robdockins
Special function support for interpreted floating point enhancement New feature or request
#159 opened Sep 22, 2021 by robdockins
3
Reimplement what4-abc using CompactGraph enhancement New feature or request
#156 opened Sep 10, 2021 by robdockins
Investigate possible exponential slowdown due to rewriting mux arrays
#153 opened Aug 25, 2021 by andreistefanescu
Adapt Verilog generator to use assign statements enhancement New feature or request
#125 opened May 21, 2021 by atomb
Primitive min/max functions enhancement New feature or request
#101 opened Feb 8, 2021 by robdockins
ProTip! Add no:assignee to see everything that’s not assigned.