diff options
author | Guy <katz911@gmail.com> | 2016-06-02 14:44:58 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-02 14:44:58 -0700 |
commit | 207a450e9a48d6cbae663d60b35594085d1a2c01 (patch) | |
tree | f897061b7417a1f6fbfffe98f1ac69b40b837f6a /src/proof | |
parent | 9712043a682572bea37099168f2c161f597b0457 (diff) |
Fixed a magical bug that only appears when compiling with clang:
The assignment
d_exprToVariableName[*it] = assignAlias(*it)
Creates an empty value for *it in d_exprToVariableName, causing the assertion in assignAlias to fail
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/bitvector_proof.cpp | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 817444ca7..268712f2a 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -628,7 +628,8 @@ void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& p if ((it->isVariable() || it->isConst()) && !ProofManager::getSkolemizationManager()->isSkolem(*it)) { d_exprToVariableName[*it] = ProofManager::sanitize(*it); } else { - d_exprToVariableName[*it] = assignAlias(*it); + std::string newAlias = assignAlias(*it); + d_exprToVariableName[*it] = newAlias; } os << "(% " << d_exprToVariableName[*it] <<" var_bv" << "\n"; @@ -1003,13 +1004,10 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os, } std::string LFSCBitVectorProof::assignAlias(Expr expr) { - static unsigned counter = 0; - if (d_exprToVariableName.find(expr) != d_exprToVariableName.end()) { - return d_exprToVariableName[expr]; - } + Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end()); std::stringstream ss; - ss << "fbv" << counter++; + ss << "fbv" << d_assignedAliases.size(); Debug("pf::bv") << "assignAlias( " << expr << ") = " << ss.str() << std::endl; d_assignedAliases[expr] = ss.str(); return ss.str(); |