Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / GaloisInc/what4 issues and pull requests

#274 - Prepare 1.6.2 release

Pull Request - State: closed - Opened by RyanGlScott 2 months ago

#273 - Support building with GHC 9.10

Pull Request - State: closed - Opened by RyanGlScott 2 months ago

#272 - Failure to compile with GHC 9.10

Issue - State: closed - Opened by ivanperez-keera 2 months ago - 1 comment

#270 - Update `tested-with` versions

Pull Request - State: closed - Opened by RyanGlScott 3 months ago

#269 - 1.6.1 release prep

Pull Request - State: closed - Opened by RyanGlScott 3 months ago - 3 comments

#268 - Inject ground values back into symbolic expressions

Pull Request - State: closed - Opened by langston-barrett 6 months ago

#267 - Improve documentation for `WordMap`

Issue - State: open - Opened by langston-barrett 6 months ago
Labels: documentation

#266 - CVC5: Don't use Tuple workaround when declaring structs

Pull Request - State: closed - Opened by RyanGlScott 6 months ago - 1 comment

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

Issue - State: closed - Opened by RyanGlScott 6 months ago - 2 comments
Labels: bug

#264 - Concretization

Pull Request - State: open - Opened by langston-barrett 6 months ago

#263 - 1.6 release prep

Pull Request - State: closed - Opened by RyanGlScott 7 months ago

#262 - what4-1.5.1 testsuite failures in stackage lts 22

Issue - State: closed - Opened by juhp 7 months ago - 3 comments

#261 - new release to allow building with ghc-9.8?

Issue - State: closed - Opened by juhp 7 months ago - 3 comments

#260 - Remove `NatRepr` arg from `resolveSymBV`

Pull Request - State: closed - Opened by langston-barrett 7 months ago - 1 comment

#259 - Concretization

Issue - State: open - Opened by langston-barrett 7 months ago - 2 comments
Labels: enhancement

#258 - Add `bv{Zero,One}` helpers, hlint config

Pull Request - State: closed - Opened by langston-barrett 8 months ago

#257 - Helpers for constructing bitvectors 0 and 1

Issue - State: closed - Opened by langston-barrett 8 months ago - 3 comments

#256 - Guard mux-pushing simplifications behind option

Pull Request - State: closed - Opened by RyanGlScott 9 months ago - 1 comment

#255 - Allow building with GHC 9.8

Pull Request - State: closed - Opened by RyanGlScott 9 months ago

#254 - Bump text dependency

Pull Request - State: closed - Opened by Vekhir 10 months ago

#252 - More simplifications

Pull Request - State: open - Opened by andreistefanescu 11 months ago

#251 - Add support for general sum types

Issue - State: open - Opened by RyanGlScott 11 months ago
Labels: enhancement

#250 - BV <> LIA translation for CHC solvers

Pull Request - State: closed - Opened by andreistefanescu 11 months ago - 1 comment

#249 - Tests for the preservation of abstract values

Issue - State: open - Opened by langston-barrett 12 months ago

#248 - Abstract values are not preserved by certain calls to `bvAdd`

Issue - State: open - Opened by langston-barrett 12 months ago - 3 comments
Labels: bug

#247 - what4: Don't annotate `{Nonce,}AppExpr`s

Pull Request - State: open - Opened by langston-barrett 12 months ago - 6 comments

#246 - Do `{Nonce,}AppExpr`s need annotations?

Issue - State: open - Opened by langston-barrett 12 months ago

#245 - what4: Don't annotate bound variables

Pull Request - State: closed - Opened by langston-barrett 12 months ago - 1 comment

#244 - Do bound variables need annotations?

Issue - State: closed - Opened by langston-barrett 12 months ago - 2 comments

#243 - 1.5.1 release prep

Pull Request - State: closed - Opened by RyanGlScott about 1 year ago

#242 - Require `versions >= 6.0.2`

Pull Request - State: closed - Opened by RyanGlScott about 1 year ago

#241 - Allow building with `versions-6.0.*`

Pull Request - State: closed - Opened by RyanGlScott about 1 year ago

#240 - Please support versions >= 6.0.1

Issue - State: closed - Opened by swt2c about 1 year ago - 7 comments

#239 - Cachix testing

Pull Request - State: closed - Opened by crdollar about 1 year ago

#238 - Cachix testing

Pull Request - State: closed - Opened by crdollar about 1 year ago

#237 - Update test.yml

Pull Request - State: closed - Opened by crdollar about 1 year ago

#236 - 1.5 release prep

Pull Request - State: closed - Opened by RyanGlScott over 1 year ago

#235 - Support building with GHC 9.6

Pull Request - State: closed - Opened by RyanGlScott over 1 year ago

#234 - Allow building with `tasty-sugar-2.2.*`

Pull Request - State: closed - Opened by RyanGlScott over 1 year ago

#233 - Allow building with `tasty-sugar-2.1.*`

Pull Request - State: closed - Opened by RyanGlScott over 1 year ago

#232 - Simplify bvult by extracting sum common when sound.

Pull Request - State: closed - Opened by andreistefanescu almost 2 years ago

#231 - Bump `what4` version to `1.4` in preparation for release

Pull Request - State: closed - Opened by RyanGlScott almost 2 years ago

#230 - Support building with GHC 9.4

Pull Request - State: closed - Opened by RyanGlScott almost 2 years ago - 2 comments

#229 - Require tasty-sugar 2.0 or greater and address deprecation.

Pull Request - State: closed - Opened by kquick almost 2 years ago - 1 comment

#228 - Use `What4.Serialize.Parser` to parse solver models/values.

Issue - State: open - Opened by andreistefanescu almost 2 years ago - 1 comment

#227 - CI: Use Nix 2.11.0

Pull Request - State: closed - Opened by RyanGlScott almost 2 years ago

#226 - SyGuS

Pull Request - State: closed - Opened by andreistefanescu almost 2 years ago - 1 comment

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

Issue - State: open - Opened by RyanGlScott almost 2 years ago
Labels: documentation

#224 - Make it build with ghc 9.4.3

Issue - State: closed - Opened by yav almost 2 years ago - 1 comment

#223 - Test problematic SMT formulas from Cryptol's `negshift` test case

Issue - State: open - Opened by RyanGlScott about 2 years ago
Labels: CI

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

Issue - State: open - Opened by RyanGlScott about 2 years ago
Labels: enhancement

#221 - Allow tasty-sugar 2.0+

Pull Request - State: closed - Opened by felixonmars about 2 years ago - 4 comments

#220 - Try splitting up `What4.Expr.Builder` to improve compile times

Issue - State: open - Opened by RyanGlScott about 2 years ago
Labels: enhancement, performance

#218 - Add `inNewFrame2`

Issue - State: open - Opened by RyanGlScott about 2 years ago
Labels: enhancement

#217 - Merge what4-serialize into what4 core

Pull Request - State: closed - Opened by travitch about 2 years ago

#216 - Use more abstract domain information in intMax/Min

Pull Request - State: closed - Opened by danmatichuk about 2 years ago - 2 comments

#215 - `intMax` is sensitive to argument ordering when applying abstract domains

Issue - State: closed - Opened by danmatichuk over 2 years ago - 1 comment

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

Issue - State: closed - Opened by arjunvish over 2 years ago - 1 comment
Labels: enhancement

#213 - Adding a feature to ask for abducts

Pull Request - State: closed - Opened by arjunvish over 2 years ago - 1 comment

#212 - Add support for transition system inputs

Pull Request - State: closed - Opened by chameco over 2 years ago - 1 comment

#211 - `template_tests`: Emit an error code if tests fail

Pull Request - State: closed - Opened by RyanGlScott over 2 years ago - 2 comments

#210 - cvc5 is too fast for challenge problem in timeout test

Issue - State: open - Opened by arjunvish over 2 years ago
Labels: bug

#209 - Problem feature lists for SMT solvers are not up to date

Issue - State: open - Opened by arjunvish over 2 years ago
Labels: enhancement

#208 - Bump copyright dates.

Pull Request - State: closed - Opened by kquick over 2 years ago

#207 - Test suites now take an hour to run after `flakes` update

Issue - State: closed - Opened by RyanGlScott over 2 years ago - 5 comments
Labels: bug, CI

#206 - `template_tests` always reports as successful, even if there are test failures

Issue - State: closed - Opened by RyanGlScott over 2 years ago - 3 comments
Labels: bug

#205 - Bump tasty-sugar version to use new 1.3 release.

Pull Request - State: closed - Opened by kquick over 2 years ago

#204 - Adding support for cvc5

Pull Request - State: closed - Opened by arjunvish over 2 years ago - 14 comments

#203 - Remove `data-binary-ieee754` dependency in favor of `GHC.Float`

Pull Request - State: closed - Opened by RyanGlScott over 2 years ago

#202 - Use `ALL` instead of `ALL_SUPPORTED`?

Issue - State: closed - Opened by RyanGlScott over 2 years ago
Labels: enhancement

#200 - Bump `what4` version to 1.3

Pull Request - State: closed - Opened by RyanGlScott over 2 years ago - 1 comment

#199 - Add operations for projecting the `SymInteger` from a `SymNat`

Pull Request - State: closed - Opened by robdockins over 2 years ago

#198 - Avoid `testProperty` deprecation warnings with `tasty-hedgehog-1.2`

Pull Request - State: closed - Opened by RyanGlScott over 2 years ago - 1 comment
Labels: tech-debt

#197 - Allow building with GHC 9.2

Pull Request - State: closed - Opened by RyanGlScott over 2 years ago

#196 - "early unsat" bookeeping error

Issue - State: open - Opened by robdockins over 2 years ago
Labels: bug

#195 - New deprecation warning

Issue - State: closed - Opened by robdockins over 2 years ago - 3 comments
Labels: tech-debt

#194 - Reconsider absorption rules for boolean predicates

Issue - State: open - Opened by robdockins over 2 years ago
Labels: tech-debt

#193 - Add pure function for getting inner integer from SymNat

Issue - State: closed - Opened by danmatichuk over 2 years ago

#192 - No interface for retrieving concrete values from annotated terms

Issue - State: closed - Opened by danmatichuk over 2 years ago - 1 comment

#191 - Fix some issues with string escaping/unescaping in the SMTLib2 writer

Pull Request - State: closed - Opened by robdockins almost 3 years ago - 2 comments

#190 - remove what4-transition-system dependency on language-sally

Pull Request - State: closed - Opened by Ptival almost 3 years ago - 1 comment

#189 - CI fails on jobs using Z3 4.8.11

Issue - State: closed - Opened by RyanGlScott almost 3 years ago - 1 comment
Labels: CI

#188 - Add support for Z3 minimization/maximization

Issue - State: open - Opened by RyanGlScott almost 3 years ago
Labels: enhancement

#187 - Add `unsafeSetAbstractValue` and `resolveSymBV`

Pull Request - State: closed - Opened by RyanGlScott almost 3 years ago - 4 comments

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

Issue - State: closed - Opened by RyanGlScott almost 3 years ago - 3 comments
Labels: tech-debt

#185 - Extended/unprintable characters when using CVC4

Issue - State: closed - Opened by finnteegen almost 3 years ago - 2 comments

#184 - String solver values when using Z3

Issue - State: closed - Opened by finnteegen almost 3 years ago - 6 comments

#183 - Don't use `rationalTerm` when ground-evaluating integers

Pull Request - State: closed - Opened by RyanGlScott almost 3 years ago - 1 comment

#181 - Export some additional operations from `What4.Expr`

Pull Request - State: closed - Opened by robdockins almost 3 years ago

#180 - Fix solver versions

Pull Request - State: closed - Opened by kquick almost 3 years ago - 5 comments

#179 - Rename the `forall` and `exists` operators to `forall_` and `exists_`

Pull Request - State: closed - Opened by robdockins almost 3 years ago

#178 - "float reduce" setting is inaccesssable

Issue - State: open - Opened by robdockins almost 3 years ago
Labels: tech-debt

#177 - Updated strings support with recent CI testing and Z3 compatibility matrix.

Pull Request - State: closed - Opened by kquick almost 3 years ago

#176 - Isolation contexts

Pull Request - State: closed - Opened by robdockins almost 3 years ago

#175 - Provide "context isolation" primitives

Issue - State: closed - Opened by robdockins almost 3 years ago - 1 comment
Labels: tech-debt

#174 - `what4:iteexprs_tests` CI failure

Issue - State: closed - Opened by RyanGlScott almost 3 years ago - 2 comments
Labels: CI

#173 - Allow building with `hashable-1.4.*`

Pull Request - State: closed - Opened by RyanGlScott almost 3 years ago

#172 - Fix Z3 tactic quoting.

Pull Request - State: closed - Opened by andreistefanescu almost 3 years ago