LeventErkok sbv issues - Githubissues

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.

https://github.com/LeventErkok/sbv

Other

242 stars 34 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Interaction performance overhead

#727 johnbender opened 2 weeks ago
27
Versions 10.11 and 10.12 don't build with GHC 9.4.8

#726 eddywestbrook opened 1 month ago
7
Design: Wp: wpProveWith: user-supplied initial state rather than a randomly generated one

#725 ocramz closed 2 months ago
1
Question: WP: `BadPrecondition` "can only happen in traceExecution"

#724 ocramz closed 2 months ago
4
Better parsing for bitwuzla output

#723 LeventErkok closed 2 months ago
1
Experimenting with data-types

#722 LeventErkok opened 2 months ago
0
potential bug in wpProveWith

#721 ocramz closed 2 months ago
2
Citing sbv

#720 ocramz closed 2 months ago
1
Overlapping instance `Queriable m (t (SBV a))`

#719 ocramz closed 2 months ago
4
Fix toSFloatingPoint simplification for AlgReal.

#718 lsrcz closed 3 months ago
1
Fix the precisions when converting a literal FP to another precision

#717 lsrcz closed 3 months ago
1
Principle of least astonishment violated for symbolic types whose metric space type differs in representation

#716 andrew-wja closed 3 months ago
9
`checkSatWith` in analogy to `satWith`

#715 andreasabel closed 2 months ago
3
Soft Question: Best approach for fixed size symbolic arrays

#714 patrickaldis closed 3 months ago
13
Remove MonadSymbolic constraint from registerUISMTFunction and smtFunName

#713 lsrcz closed 3 months ago
0
Document the known issue of the registration uninterpreted functions

#712 lsrcz closed 3 months ago
1
Using uninterpreted functions in a quantified formula will not declare it in the top-level

#711 lsrcz closed 3 months ago
10
Let 'optimize' return variable values

#710 amigalemming closed 3 months ago
2
OptimizeStyle: add type parameter for the optimize result type

#709 thielema closed 3 months ago
2
Ranges over SIntegers

#708 Torrencem closed 3 months ago
4
Make OptimizeResult type dependent on OptimizeStyle

#707 amigalemming closed 3 months ago
3
Consider removing `Num a => Num (SBV a)` instance

#706 LeventErkok closed 4 months ago
0
Explore `Iso` instances

#705 LeventErkok closed 2 months ago
4
FAQ: best practices for records?

#704 andreasabel closed 4 months ago
4
Fix the total order comparison for arbitrary floating point

#703 lsrcz closed 4 months ago
0
Unsound term simplification for ite with SFloatingPoint

#702 lsrcz closed 4 months ago
2
Fix the Ord instance for FP and FloatingPoint

#701 lsrcz closed 4 months ago
2
Fix mkConstCV which uses fromInteger for FP.

#700 lsrcz closed 4 months ago
1
CFP case missing in the Eq instance for CVal

#699 lsrcz closed 4 months ago
5
Generating `Num (SBV a)` instances "generically"

#698 andreasabel closed 3 months ago
10
Q: Results of 'wpProveWith'

#697 ocramz closed 5 months ago
2
Tower example

#696 LeventErkok closed 5 months ago
0
Try to fix the zombie solver processes, don't hide the exceptions

#695 lsrcz closed 5 months ago
0
Zombie process fixes

#694 LeventErkok closed 5 months ago
5
Revert "Fix the zombie solver processes mentioned in #477"

#693 LeventErkok closed 5 months ago
0
ExtractIO

#692 LeventErkok closed 5 months ago
1
Fix the zombie solver processes mentioned in #477

#691 lsrcz closed 5 months ago
2
Set support for cvc5

#690 paulbrauner-da closed 6 months ago
1
Adding useful type-class instances for NonEmpty

#689 recursion-ninja closed 5 months ago
1
Create `NonEmpty` instances for `EqSymbolic`, `OrdSymbolic`, `Mergeable`, etc.

#688 recursion-ninja closed 5 months ago
0
SBV->C: Support arbitrary size bit-vectors, and in general all(?) SBV types

#687 yav opened 6 months ago
10
GH pages link leads to 404

#686 fabeulous closed 6 months ago
1
CrackNum decimal printing

#685 LeventErkok closed 7 months ago
3
Fix SMTDefinable instances for 8-arg through 12-arg uninterpreted functions

#684 octalsrc closed 7 months ago
1
Fix CVC5 list parsing

#683 LeventErkok closed 7 months ago
2
Query mode: Calls to `getValue` might need calling `ensureSat` first

#682 LeventErkok closed 8 months ago
0
Issue with initializing state with multiple symbolic arrays

#681 lucaspena closed 8 months ago
5
Re-enable sbv on stackage

#680 lsrcz closed 9 months ago
4
SArray scoping issue / weird SMT error

#679 Torrencem closed 9 months ago
6
SBV 10.3 release

#678 LeventErkok closed 10 months ago
1