Skip to content

Crucible support as a Symbolic Engine #37

Description

@rafaelsamenezes

Is your feature request related to a problem? Please describe.
Currently, we only have support for KLEE as a symbolic engine, the issue is that it contains a limitation for floating numbers. Crucible supports enconding for floats, has support for SV-COMP notation and it's API contains all that is needed for a Generator.

Describe the solution you'd like
Implement a NonDetGeneratorCrucible and compare it with KLEE specially for floats.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

enhancementgood-first-issueissues that do not need great knowledge about Map2Check or are easy to implement

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions