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

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 817444ca7d8d43d5f337a4c4034837ccd56c0539..268712f2a8ee07418d2f2826352a1329ed19e490 100644 (file)
--- 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();