| 41 | } |
| 42 | |
| 43 | smtutil::Expression nondetInterface( |
| 44 | Predicate const& _pred, |
| 45 | ContractDefinition const& _contract, |
| 46 | EncodingContext& _context, |
| 47 | unsigned _preIdx, |
| 48 | unsigned _postIdx) |
| 49 | { |
| 50 | auto const& state = _context.state(); |
| 51 | std::vector<smtutil::Expression> stateExprs = getStateExpressionsForNondetInterface(state); |
| 52 | return _pred( |
| 53 | stateExprs + |
| 54 | std::vector<smtutil::Expression>{_context.state().state(_preIdx)} + |
| 55 | stateVariablesAtIndex(_preIdx, _contract, _context) + |
| 56 | std::vector<smtutil::Expression>{_context.state().state(_postIdx)} + |
| 57 | stateVariablesAtIndex(_postIdx, _contract, _context) |
| 58 | ); |
| 59 | } |
| 60 | |
| 61 | smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _context) |
| 62 | { |
no test coverage detected