This repository's issues are reserved for feature requests and bug reports.
-
I'm submitting a ...
-
What is the current behavior?
UnSat Core type is a [String]. This is makes the type rigid and forces special operations on the type whereas a more extensible solution is to re-use the result type in Result.hs. At the moment this is a technological limitation of SBV
-
If the current behavior is a bug, please provide the steps to reproduce and if possible a minimal demo of the problem via
https://plnkr.co or similar (you can use this template as a starting point: http://plnkr.co/edit/tpl:AvJOMERrnz94ekVua0u5).
-
What is the expected behavior?
-
What is the motivation / use case for changing the behavior?
-
Please tell us about your environment:
- Version: 2.0.0-beta.X
- OS: [MacOSX | Windows 10 | Windows 7 | Linux (specify distro)]
- GHC Version:
- Solver: [ Z3 | Yices | MathSat | Boolector | ABC | Cvc4 ]
- Solver Version:
-
Other information (e.g. detailed explanation, stacktraces, related issues, suggestions how to fix, links for us to have context, eg. stackoverflow, gitter, etc)
This repository's issues are reserved for feature requests and bug reports.
I'm submitting a ...
What is the current behavior?
UnSat Core type is a [String]. This is makes the type rigid and forces special operations on the type whereas a more extensible solution is to re-use the result type in Result.hs. At the moment this is a technological limitation of SBV
If the current behavior is a bug, please provide the steps to reproduce and if possible a minimal demo of the problem via
https://plnkr.co or similar (you can use this template as a starting point: http://plnkr.co/edit/tpl:AvJOMERrnz94ekVua0u5).
What is the expected behavior?
What is the motivation / use case for changing the behavior?
Please tell us about your environment:
Other information (e.g. detailed explanation, stacktraces, related issues, suggestions how to fix, links for us to have context, eg. stackoverflow, gitter, etc)