Skip to content

Detect default solver #1820

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

Merged
ehennenfent merged 3 commits into from
Nov 6, 2020
Merged

Detect default solver #1820

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
e112a02
Detect default solver: try yices, if not present use z3
montyly Nov 6, 2020
fd9927a
Update solver.py
montyly Nov 6, 2020
955ab90
Update message about solver selection
Nov 6, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -229,10 +229,10 @@ for idx, val_list in enumerate(m.collect_returns()):
* We're still in the process of implementing full support for the EVM Istanbul instruction semantics, so certain opcodes may not be supported.
In a pinch, you can try compiling with Solidity 0.4.x to avoid generating those instructions.

## Using a different solver (Z3, Yices, CVC4)
## Using a different solver (Yices, Z3, CVC4)
Manticore relies on an external solver supporting smtlib2. Currently Z3, Yices and CVC4 are supported and can be selected via commandline or configuration settings.
By default Manticore will use Z3. Once you've installed a different solver, you can choose which one to use like this:
```manticore --smt.solver yices```
If Yices is available, Manticore will use it by default. If not, it will fall back to Z3 or CVC4. If you want to manually choose which solver to use, you can do so like this:
```manticore --smt.solver Z3```
### Installing CVC4
For more details go to https://cvc4.github.io/. Otherwise just get the binary and use it.

Expand Down
2 changes: 1 addition & 1 deletion manticore/core/smtlib/solver.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ class SolverType(config.ConfigEnum):

consts.add(
"solver",
default=SolverType.z3,
default=SolverType.auto,
description="Choose default smtlib2 solver (z3, yices, cvc4, auto)",
)

Expand Down