| 748 | } |
| 749 | |
| 750 | void SMTEncoder::initContract(ContractDefinition const& _contract) |
| 751 | { |
| 752 | solAssert(m_currentContract == nullptr, ""); |
| 753 | m_currentContract = &_contract; |
| 754 | |
| 755 | m_context.reset(); |
| 756 | m_context.pushSolver(); |
| 757 | createStateVariables(_contract); |
| 758 | clearIndices(m_currentContract, nullptr); |
| 759 | m_checked = true; |
| 760 | } |
| 761 | |
| 762 | void SMTEncoder::initFunction(FunctionDefinition const& _function) |
| 763 | { |
nothing calls this directly
no test coverage detected