Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Make the Crucible backend parametric in the SMT solver #1520

Closed
andreistefanescu opened this issue Nov 23, 2021 · 1 comment
Closed

Make the Crucible backend parametric in the SMT solver #1520

andreistefanescu opened this issue Nov 23, 2021 · 1 comment
Assignees
@robdockins
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm

Comments

@andreistefanescu
Copy link
Contributor

#1515 switches the SMT solver used during the Crucible symbolic execution from Yices to Z3:

saw-script/src/SAWScript/Crucible/Common.hs

Line 43 in 608c65e

type Sym = OnlineBackendUserSt Nonce.GlobalNonceGenerator Yices.Connection SAWCoreState (W4.Flags W4.FloatReal)

Let's make the Crucible backend parametric in the SMT solver. This it not as easy as it could be because the SMT solver choice is part of the type of the backend.
@andreistefanescu andreistefanescu added the subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm label Nov 23, 2021
@andreistefanescu andreistefanescu mentioned this issue Nov 23, 2021
Merged
@robdockins robdockins self-assigned this May 19, 2022
@robdockins
Copy link
Contributor

Fixed via #1672. The new (experimental) set_path_sat_solver command allows users to select which solver to use for path-sat checking. Currently only Z3 and Yices are supported, but it would be relatively easy to add others.

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

@robdockins robdockins

Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@andreistefanescu @robdockins