GaloisInc/what4

Issues

• Failure to compile with GHC 9.10

  #272 opened 3 months ago by ivanperez-keera
  1

• What4 over-eagerly produces counterexamples with `ArrayMapping` instead of `ArrayConcrete`

  #271 opened 3 months ago by RyanGlScott
  0

• Concretization

  #259 opened 8 months ago by langston-barrett
  2

• Improve documentation for `WordMap`

  #267 opened 6 months ago by langston-barrett
  0

• CVC5 fails to parse `what4`-generated SMT-LIB for constructing and selecting tuples

  #265 opened 6 months ago by RyanGlScott
  2

• new release to allow building with ghc-9.8?

  #261 opened 7 months ago by juhp
  3

• what4-1.5.1 testsuite failures in stackage lts 22

  #262 opened 7 months ago by juhp
  3

• Helpers for constructing bitvectors 0 and 1

  #257 opened 8 months ago by langston-barrett
  3

• Document Builder expression simplifications

  #253 opened a year ago by andreistefanescu
  0

• Add support for general sum types

  #251 opened a year ago by RyanGlScott
  0

• cvc5 is too fast for challenge problem in timeout test

  #210 opened 2 years ago by arjunvish
  0

• Abstract values are not preserved by certain calls to `bvAdd`

  #248 opened a year ago by langston-barrett
  3

• Tests for the preservation of abstract values

  #249 opened a year ago by langston-barrett
  0

• Do bound variables need annotations?

  #244 opened a year ago by langston-barrett
  2

• Do `{Nonce,}AppExpr`s need annotations?

  #246 opened a year ago by langston-barrett
  0

• Please support versions >= 6.0.1

  #240 opened a year ago by swt2c
  7

• Make it build with ghc 9.4.3

  #224 opened 2 years ago by yav
  1

• Use `What4.Serialize.Parser` to parse solver models/values.

  #228 opened 2 years ago by andreistefanescu
  1

• Incorrect documentation for little-endian functions in `What4.SWord`

  #225 opened 2 years ago by RyanGlScott
  0

• Test problematic SMT formulas from Cryptol's `negshift` test case

  #223 opened 2 years ago by RyanGlScott
  0

• Support SMT-LIB's `str.to_code` and `str.from_code` functions over strings

  #222 opened 2 years ago by RyanGlScott
  0

• Try splitting up `What4.Expr.Builder` to improve compile times

  #220 opened 2 years ago by RyanGlScott
  0

• Add `inNewFrame2`

  #218 opened 2 years ago by RyanGlScott
  0

• cvc5 bug prevents `unsat-cores` and `produce-abducts` being turned on simultaneously

  #214 opened 2 years ago by arjunvish
  1

• `intMax` is sensitive to argument ordering when applying abstract domains

  #215 opened 2 years ago by danmatichuk
  1

• `template_tests` always reports as successful, even if there are test failures

  #206 opened 2 years ago by RyanGlScott
  3

• Problem feature lists for SMT solvers are not up to date

  #209 opened 2 years ago by arjunvish
  0

• Use `ALL` instead of `ALL_SUPPORTED`?

  #202 opened 2 years ago by RyanGlScott
  0

• Test suites now take an hour to run after `flakes` update

  #207 opened 2 years ago by RyanGlScott
  5

• Break dependency loop by moving `What4.TransitionSystem.Exporter.Sally` to `language-sally`

  #186 opened 3 years ago by RyanGlScott
  3

• No interface for retrieving concrete values from annotated terms

  #192 opened 3 years ago by danmatichuk
  1

• Add pure function for getting inner integer from SymNat

  #193 opened 3 years ago by danmatichuk
  0

• New deprecation warning

  #195 opened 3 years ago by robdockins
  3

• CI fails on jobs using Z3 4.8.11

  #189 opened 3 years ago by RyanGlScott
  1

• "early unsat" bookeeping error

  #196 opened 3 years ago by robdockins
  0

• String solver values when using Z3

  #184 opened 3 years ago by finnteegen
  6

• Extended/unprintable characters when using CVC4

  #185 opened 3 years ago by finnteegen
  2

• Reconsider absorption rules for boolean predicates

  #194 opened 3 years ago by robdockins
  0

• Add support for Z3 minimization/maximization

  #188 opened 3 years ago by RyanGlScott
  0

• CVC4 backend fails to parse `groundEval` of `Int`-indexed array (`array select not indexed with correct type for array`)

  #182 opened 3 years ago by RyanGlScott
  2

• "float reduce" setting is inaccesssable

  #178 opened 3 years ago by robdockins
  0

• Provide "context isolation" primitives

  #175 opened 3 years ago by robdockins
  1

• GHC will claim the `forall` identifier

  #166 opened 3 years ago by robdockins
  0

• `what4:iteexprs_tests` CI failure

  #174 opened 3 years ago by RyanGlScott
  2

• CI failure on GHC 8.6.5 only (`libz.so: cannot open shared object file: No such file or directory`)

  #169 opened 3 years ago by RyanGlScott
  4

• Special function support for interpreted floating point

  #159 opened 3 years ago by robdockins
  3

• What4 update results in new exception from an FnArrayTypeMap in an if/then/else on test run with Yices

  #157 opened 3 years ago by bboston7
  2

• what4-abc fails to compile due to missing cases for `CopyArray` and friends

  #154 opened 3 years ago by RyanGlScott
  0

• Reimplement what4-abc using CompactGraph

  #156 opened 3 years ago by robdockins
  0

• Investigate possible exponential slowdown due to rewriting mux arrays

  #153 opened 3 years ago by andreistefanescu
  0