Add assert for both branches in mergeVariables in SMTChecker

This commit is contained in:
Alex Beregszaszi 2018-07-24 22:43:05 +01:00
parent ae0959ae12
commit 278372c13d

View File

@ -752,6 +752,7 @@ void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _varia
set<VariableDeclaration const*> uniqueVars(_variables.begin(), _variables.end());
for (auto const* decl: uniqueVars)
{
solAssert(_countersEndTrue.count(decl) && _countersEndFalse.count(decl), "");
int trueCounter = _countersEndTrue.at(decl).index();
int falseCounter = _countersEndFalse.at(decl).index();
solAssert(trueCounter != falseCounter, "");