diff --git a/docs/docs/core.md b/docs/docs/core.md index 7688e49..03a9a1d 100644 --- a/docs/docs/core.md +++ b/docs/docs/core.md @@ -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 @@ -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`. \ No newline at end of file +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`.