issues
search
GaloisInc
/
what4
Symbolic formula representation and solver interaction library
155
stars
13
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Prepare 1.6.2 release
#274
RyanGlScott
closed
2 months ago
0
Support building with GHC 9.10
#273
RyanGlScott
closed
2 months ago
0
Failure to compile with GHC 9.10
#272
ivanperez-keera
closed
2 months ago
1
What4 over-eagerly produces counterexamples with `ArrayMapping` instead of `ArrayConcrete`
#271
RyanGlScott
opened
2 months ago
0
Update `tested-with` versions
#270
RyanGlScott
closed
2 months ago
0
1.6.1 release prep
#269
RyanGlScott
closed
2 months ago
3
Inject ground values back into symbolic expressions
#268
langston-barrett
closed
5 months ago
0
Improve documentation for `WordMap`
#267
langston-barrett
opened
5 months ago
0
CVC5: Don't use Tuple workaround when declaring structs
#266
RyanGlScott
closed
5 months ago
1
CVC5 fails to parse `what4`-generated SMT-LIB for constructing and selecting tuples
#265
RyanGlScott
closed
5 months ago
2
Concretization
#264
langston-barrett
opened
6 months ago
0
1.6 release prep
#263
RyanGlScott
closed
6 months ago
0
what4-1.5.1 testsuite failures in stackage lts 22
#262
juhp
closed
6 months ago
3
new release to allow building with ghc-9.8?
#261
juhp
closed
6 months ago
3
Remove `NatRepr` arg from `resolveSymBV`
#260
langston-barrett
closed
7 months ago
1
Concretization
#259
langston-barrett
opened
7 months ago
2
Add `bv{Zero,One}` helpers, hlint config
#258
langston-barrett
closed
7 months ago
0
Helpers for constructing bitvectors 0 and 1
#257
langston-barrett
closed
7 months ago
3
Guard mux-pushing simplifications behind option
#256
RyanGlScott
closed
6 months ago
1
Allow building with GHC 9.8
#255
RyanGlScott
closed
8 months ago
0
Bump text dependency
#254
Vekhir
closed
9 months ago
0
Document Builder expression simplifications
#253
andreistefanescu
opened
10 months ago
0
More simplifications
#252
andreistefanescu
closed
10 months ago
1
Add support for general sum types
#251
RyanGlScott
opened
10 months ago
0
BV <> LIA translation for CHC solvers
#250
andreistefanescu
closed
10 months ago
1
Tests for the preservation of abstract values
#249
langston-barrett
opened
11 months ago
0
Abstract values are not preserved by certain calls to `bvAdd`
#248
langston-barrett
opened
11 months ago
3
what4: Don't annotate `{Nonce,}AppExpr`s
#247
langston-barrett
opened
11 months ago
6
Do `{Nonce,}AppExpr`s need annotations?
#246
langston-barrett
opened
11 months ago
0
what4: Don't annotate bound variables
#245
langston-barrett
closed
11 months ago
1
Do bound variables need annotations?
#244
langston-barrett
closed
11 months ago
2
1.5.1 release prep
#243
RyanGlScott
closed
1 year ago
0
Require `versions >= 6.0.2`
#242
RyanGlScott
closed
1 year ago
0
Allow building with `versions-6.0.*`
#241
RyanGlScott
closed
1 year ago
0
Please support versions >= 6.0.1
#240
swt2c
closed
1 year ago
7
Cachix testing
#239
crdollar
closed
1 year ago
0
Cachix testing
#238
crdollar
closed
1 year ago
0
Update test.yml
#237
crdollar
closed
1 year ago
0
1.5 release prep
#236
RyanGlScott
closed
1 year ago
0
Support building with GHC 9.6
#235
RyanGlScott
closed
1 year ago
0
Allow building with `tasty-sugar-2.2.*`
#234
RyanGlScott
closed
1 year ago
0
Allow building with `tasty-sugar-2.1.*`
#233
RyanGlScott
closed
1 year ago
0
Simplify bvult by extracting sum common when sound.
#232
andreistefanescu
closed
1 year ago
0
Bump `what4` version to `1.4` in preparation for release
#231
RyanGlScott
closed
1 year ago
0
Support building with GHC 9.4
#230
RyanGlScott
closed
1 year ago
2
Require tasty-sugar 2.0 or greater and address deprecation.
#229
kquick
closed
1 year ago
1
Use `What4.Serialize.Parser` to parse solver models/values.
#228
andreistefanescu
opened
1 year ago
1
CI: Use Nix 2.11.0
#227
RyanGlScott
closed
1 year ago
0
SyGuS
#226
andreistefanescu
closed
1 year ago
1
Incorrect documentation for little-endian functions in `What4.SWord`
#225
RyanGlScott
opened
1 year ago
0
Next