Free assumptions weren't getting cleaned up due to not doing a postorder traversal. This issue came up when doing subproof sharing involving SCOPE proofs.
}
// will need to unbind the variables below
visited[cur] = false;
}
// will need to unbind the variables below
visited[cur] = false;
}
// The following loop cannot be merged with the loop above because the
// same subproof
}
// The following loop cannot be merged with the loop above because the
// same subproof
}
else if (!it->second)
{
}
else if (!it->second)
{
Assert(cur->getRule() == PfRule::SCOPE);
// unbind its assumptions
for (const Node& a : cargs)
Assert(cur->getRule() == PfRule::SCOPE);
// unbind its assumptions
for (const Node& a : cargs)