| 2561 | } |
| 2562 | |
| 2563 | smtutil::Expression SMTEncoder::expr(Expression const& _e, Type const* _targetType) |
| 2564 | { |
| 2565 | if (!m_context.knownExpression(_e)) |
| 2566 | { |
| 2567 | m_unsupportedErrors.warning(6031_error, _e.location(), "Internal error: Expression undefined for SMT solver." ); |
| 2568 | createExpr(_e); |
| 2569 | } |
| 2570 | |
| 2571 | return m_context.expression(_e)->currentValue(underlyingType(_targetType)); |
| 2572 | } |
| 2573 | |
| 2574 | void SMTEncoder::createExpr(Expression const& _e) |
| 2575 | { |
no test coverage detected