Skip to content

Issues: runtimeverification/haskell-backend

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

135 Open 1,169 Closed
135 Open 1,169 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

Booster's simplifier is unable to prune a #Bottom state enhancement New feature or request
#4067 opened Oct 29, 2024 by geo2a
Use smart Pattern constructor throughout the code
#4065 opened Oct 23, 2024 by jberthold
Add a lightweight check for requires of equations when matching is indeterminate booster Relates to booster code enhancement New feature or request
#4053 opened Sep 27, 2024 by geo2a
Dynamic prelude
#4034 opened Aug 14, 2024 by PetarMax
4
booster-dev crashes on simple test
#4023 opened Aug 8, 2024 by ehildenb
1
Make the "simplify" endpoint in Booster evaluate inconsisten predicates and patterns to #Bottom
#4012 opened Aug 1, 2024 by geo2a
2
Run test-prove-functional as part of performance-test-kevm.sh
#4005 opened Jul 29, 2024 by geo2a
Extend log processing tools to quantify _phases_ of execution
#3994 opened Jul 24, 2024 by jberthold
Implies request (from kontrol) taking 1h to process
#3990 opened Jul 22, 2024 by jberthold
@goodlyrottenapple
Modify performance scripts to run with sequential prover
#3972 opened Jul 9, 2024 by geo2a
Compute remainders in booster
#3956 opened Jun 21, 2024 by goodlyrottenapple
Reasoning about remainders bug
#3948 opened Jun 18, 2024 by PetarMax
@PetarMax
3
Investigate the background of #3917 (injections and SMT)
#3920 opened Jun 5, 2024 by jberthold
Make SMT timeout increase strategy configurable
#3910 opened May 31, 2024 by geo2a
Enable using cvc5 SMT solver in Kore
#3905 opened May 28, 2024 by geo2a
2
Treat all terms of sort Bool as Predicate in "get-model" booster Relates to booster code
#3903 opened May 27, 2024 by geo2a
Create a profiler leveraging the contextual logging
#3888 opened May 22, 2024 by geo2a
3
Add "hard" integration test for Booster's SMT solver interface
#3887 opened May 22, 2024 by geo2a
Non-terminating simplifications bug
#3873 opened May 15, 2024 by PetarMax
1
Remove log-failed-rewrites "execute" request parameter cleanup
#3872 opened May 15, 2024 by geo2a
Extend definedness analysis to equations and output results in user-friendly way
#3868 opened May 15, 2024 by jberthold
@goodlyrottenapple
Improving pre-SMT reasoning capabilities enhancement New feature or request
#3861 opened May 14, 2024 by PetarMax
1
8
Booster's and Kore's "implies" endpoints disagree on a pyk integration test
#3857 opened May 10, 2024 by geo2a
3
Improve implication endpoint in booster
#3854 opened May 9, 2024 by goodlyrottenapple
2
Booster: Add internalised representations for Int and Bool
#3848 opened May 3, 2024 by jberthold
ProTip! Adding no:label will show everything without a label.