| 2515 | } |
| 2516 | |
| 2517 | void SMTEncoder::mergeVariables(smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) |
| 2518 | { |
| 2519 | for (auto const& entry: _indicesEndTrue) |
| 2520 | { |
| 2521 | VariableDeclaration const* var = entry.first; |
| 2522 | auto trueIndex = entry.second; |
| 2523 | if (_indicesEndFalse.count(var) && _indicesEndFalse.at(var) != trueIndex) |
| 2524 | { |
| 2525 | m_context.addAssertion(m_context.newValue(*var) == smtutil::Expression::ite( |
| 2526 | _condition, |
| 2527 | valueAtIndex(*var, trueIndex), |
| 2528 | valueAtIndex(*var, _indicesEndFalse.at(var))) |
| 2529 | ); |
| 2530 | } |
| 2531 | } |
| 2532 | } |
| 2533 | |
| 2534 | smtutil::Expression SMTEncoder::currentValue(VariableDeclaration const& _decl) const |
| 2535 | { |
nothing calls this directly
no test coverage detected