Skip to content

Commit

Permalink
Typo in core.md
Browse files Browse the repository at this point in the history
  • Loading branch information
bossjoker1 authored Oct 30, 2024
1 parent 1c9ca67 commit 89c53c0
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions docs/docs/core.md
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,7 @@ A state offers many API for its inspection:

```python
>>> entry_state.curr_stmt # print the current statement ready for execution
>>> entry_state.revert # weather the state reverted or not
>>> entry_state.revert # whether the state reverted or not
>>> entry_state.instruction_count # how many instructions have been executed up to this point
>>> entry_state.pc # current program counter
>>> entry_state.registers # overview of all the virtual registers defined during the execution up to this point
Expand Down Expand Up @@ -162,4 +162,4 @@ The default solver employed by greed is [Yices2](https://github.com/SRI-CSL/yice
We made this decision based on the impressive results obtained in the latest SMT solving competition, and based on the results showed by Frank et al. in [ETHBMC](https://www.usenix.org/system/files/sec20fall_frank_prepub_0.pdf).
That being said, greed offers a modular architecure and implementing support for a new solver backend is quite straigthforward.

By default, we give unlimited time to the solver to solve the constraints. However, it can be sometimes helpful to timeout after a certain amount of time. You can do this by using the option `SOLVER_TIMEOUT`. Keep in mind that, when the timeout fires, the state will be reported as `errored`.
By default, we give unlimited time to the solver to solve the constraints. However, it can be sometimes helpful to timeout after a certain amount of time. You can do this by using the option `SOLVER_TIMEOUT`. Keep in mind that, when the timeout fires, the state will be reported as `errored`.

0 comments on commit 89c53c0

Please sign in to comment.