runtimeverification/haskell-backend

Issues

• Booster's simplifier is unable to prune a `#Bottom` state

  #4067 opened 2 months ago by geo2a
  1

• Reasoning about remainders

  #3948 opened 6 months ago by PetarMax
  3

• Compute remainders in booster

  #3956 opened 6 months ago by goodlyrottenapple
  0

• Make the `"simplify`" endpoint in Booster evaluate inconsisten predicates and patterns to `#Bottom`

  #4012 opened 5 months ago by geo2a
  0

• Use smart `Pattern` constructor throughout the code

  #4065 opened 2 months ago by jberthold
  0

• Recognise ensured constraints as substitutions and apply them in `Booster`

  #4059 opened 2 months ago by geo2a
  1

• Add a lightweight check for `requires` of equations when matching is indeterminate

  #4053 opened 3 months ago by geo2a
  0

• Dynamic prelude

  #4034 opened 4 months ago by PetarMax
  4

• Optimising SAT checks

  #3952 opened 4 months ago by PetarMax
  6

• Booster: Optimise handling of known predicates when rewriting

  #4029 opened 4 months ago by geo2a
  3

• Booster: only check the SMT prelude once, on server start

  #4036 opened 4 months ago by geo2a
  0

• Preserve clause ordering of `requires` and `ensures` when internalisig rules

  #4028 opened 4 months ago by geo2a
  0

• Pass `--smt-arg` to Kore's SMT solver

  #4024 opened 4 months ago by geo2a
  0

• Add a few tests for booster's implication endpoint

  #3869 opened 4 months ago by jberthold
  0

• Regression in the `implies` endpoint of `booster-dev`

  #3941 opened 4 months ago by tothtamas28
  1

• `booster-dev` crashes on simple test

  #4023 opened 5 months ago by ehildenb
  1

• SMT retry count set to 3 when `--smt-retry-limit 0` is passed

  #3991 opened 5 months ago by geo2a
  0

• Experiment: Cache lookup chaining (for booster equation cache)

  #3982 opened 5 months ago by jberthold
  0

• Booster: consider path condition for simplification cache

  #3993 opened 5 months ago by jberthold
  0

• Name collision for existential variables

  #4006 opened 5 months ago by jberthold
  0

• Run `test-prove-functional` as part of `performance-test-kevm.sh`

  #4005 opened 5 months ago by geo2a
  0

• Extend log processing tools to quantify _phases_ of execution

  #3994 opened 5 months ago by jberthold
  0

• Implies request (from kontrol) taking 1h to process

  #3990 opened 5 months ago by jberthold
  0

• Filter requires clause a second time when applyin rewrite rules in Booster

  #3886 opened 5 months ago by geo2a
  0

• Use the SMT solver when checking equations' side condtions in Booster

  #3902 opened 5 months ago by geo2a
  1

• Z3 zombie processes during long proofs

  #3959 opened 5 months ago by jberthold
  2

• Utilise new sequence folder structure in bug reports in kore-rpc-client

  #3978 opened 5 months ago by goodlyrottenapple
  0

• `Proxy.hs` loses information when pruning branches

  #3973 opened 5 months ago by geo2a
  0

• Modify performance scripts to run with sequential prover

  #3972 opened 6 months ago by geo2a
  0

• Add `[depth]` logging context

  #3885 opened 6 months ago by geo2a
  0

• Stabilise normalisation of `Int`comparison operators

  #3938 opened 6 months ago by PetarMax
  9

• Haskell backend booster returning a doubled substitution

  #3912 opened 6 months ago by ehildenb
  10

• Annoying warning about recursion depth being exceeded

  #3927 opened 6 months ago by ehildenb
  1

• Crash in SMT solver on input during execute request

  #3934 opened 6 months ago by ehildenb
  2

• Consolidate `--log-format json` and `--log-timestamps` options

  #3894 opened 6 months ago by geo2a
  0

• Return rule label even if rule id is not present

  #3913 opened 7 months ago by ehildenb
  1

• Investigate the background of #3917 (injections and SMT)

  #3920 opened 7 months ago by jberthold
  0

• SMT problem: line 2 column 232: Sorts SortStatusCode and SortEndStatusCode are incompatible

  #3917 opened 7 months ago by jinxinglim
  0

• Retry Booster's SMT queries

  #3884 opened 7 months ago by geo2a
  0

• Create a profiler leveraging the contextual logging

  #3888 opened 7 months ago by geo2a
  3

• Enable using `cvc5` SMT solver in Kore

  #3905 opened 7 months ago by geo2a
  2

• How to determine from logs why higher-priority rule isn't being applied

  #3909 opened 7 months ago by ehildenb
  6

• Make SMT timeout increase strategy configurable

  #3910 opened 7 months ago by geo2a
  0

• Treat all terms of sort `Bool` as `Predicate` in `"get-model"`

  #3903 opened 7 months ago by geo2a
  0

• Booster: More flexible rewrite rule indexing

  #3874 opened 7 months ago by jberthold
  0

• Missing implementation for `MAP.updateAll` in legacy kore

  #3898 opened 7 months ago by jberthold
  0

• Add "hard" integration test for Booster's SMT solver interface

  #3887 opened 7 months ago by geo2a
  0

• Remove code that collects and returns RPC simplification logs

  #3871 opened 7 months ago by geo2a
  2

• Non-terminating simplifications

  #3873 opened 7 months ago by PetarMax
  1

• Remove `log-failed-rewrites` "execute" request parameter

  #3872 opened 7 months ago by geo2a
  0