GaloisInc/what4 issues and pull requests

#171 - CI update to lock nix version

Pull Request - State: closed - Opened by kquick about 3 years ago - 1 comment

#170 - Draft: Try bumping cache version (#169)

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

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

Issue - State: closed - Opened by RyanGlScott about 3 years ago - 4 comments
Labels: CI

#168 - Add Z3 tactic option.

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

#167 - Simplify array lookup of update with symbolic index.

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

#166 - GHC will claim the `forall` identifier

Issue - State: closed - Opened by robdockins about 3 years ago

#165 - Add ceiling and floor special functions

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

#164 - Minor fixes to `Atan2`, `Pow` handling in `realSpecialFunction`

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

#163 - Add `pow` (`x^y`) as a `SpecialFunction`

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

#162 - Reduce memory usage for `WeightedSum` values.

Pull Request - State: closed - Opened by brianhuffman about 3 years ago - 1 comment

#161 - Add missing Foldable, Traversable, and Show instances for LabeledPred

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

#160 - Special functions

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

#159 - Special function support for interpreted floating point

Issue - State: open - Opened by robdockins about 3 years ago - 3 comments
Labels: enhancement

#158 - Fix syntax errors in Verilog variable names

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

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

Issue - State: closed - Opened by bboston7 about 3 years ago - 2 comments

#156 - Reimplement what4-abc using CompactGraph

Issue - State: open - Opened by robdockins about 3 years ago
Labels: enhancement

#155 - Add ConcreteFloat constructor

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

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

Issue - State: closed - Opened by RyanGlScott about 3 years ago

#153 - Investigate possible exponential slowdown due to rewriting mux arrays

Issue - State: open - Opened by andreistefanescu over 3 years ago

#152 - Add arrayCopy, arraySet, and arrayRangeEqual primitives.

Pull Request - State: closed - Opened by andreistefanescu over 3 years ago - 1 comment

#151 - Expose the uninterpreted constants in a SymExpr.

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

#150 - Add Z3 version matrix and cachix caching.

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

#149 - CI with Z3 4.8.11

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

#148 - Remove obsolete boolector command-line option

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

#147 - String updates

Pull Request - State: closed - Opened by robdockins over 3 years ago - 5 comments

#146 - Add `ProblemFeature` values

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

#145 - Test failures with Boolector 3.2.2

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

#144 - CVC4 array fix

Pull Request - State: closed - Opened by robdockins over 3 years ago - 1 comment

#140 - Add to Stackage

Issue - State: closed - Opened by t4ccer over 3 years ago - 2 comments

#139 - Problem feature for uninterpreted functions

Issue - State: closed - Opened by robdockins over 3 years ago
Labels: enhancement

#138 - multi-dimensional array type mismatch for CVC4 backend

Issue - State: closed - Opened by dmwit over 3 years ago - 1 comment
Labels: bug

#137 - `ConcreteVal` constructor for floating-point values

Issue - State: closed - Opened by robdockins over 3 years ago
Labels: enhancement

#132 - Test failure with Z3 4.8.11

Issue - State: closed - Opened by felixonmars over 3 years ago - 1 comment
Labels: upstream, tech-debt

#124 - Add a solver adapter for bitwuzla

Pull Request - State: closed - Opened by travitch over 3 years ago - 4 comments

#104 - Merge the what4-serialize repository into what4

Issue - State: closed - Opened by travitch almost 4 years ago
Labels: tech-debt

#73 - Z3: structs not being declared, or being redundantly declared when using multi-dimensional arrays

Issue - State: closed - Opened by danmatichuk about 4 years ago - 5 comments
Labels: bug

#56 - SMT String literal escaping

Issue - State: closed - Opened by robdockins over 4 years ago - 4 comments
Labels: enhancement, upstream

#10 - Add more simplifications for adjacent `ite` expressions

Issue - State: open - Opened by brianhuffman almost 5 years ago - 1 comment
Labels: enhancement, good first issue

#6 - Extend symbolic string support to 8-bit and 16-bit strings

Issue - State: open - Opened by robdockins over 5 years ago - 9 comments
Labels: enhancement

GitHub / GaloisInc/what4 issues and pull requests