Fix

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 479266db4e16b249895d063bdfa40a36892dd621..817444ca7d8d43d5f337a4c4034837ccd56c0539 100644 (file)
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -1004,7 +1004,10 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
 
 std::string LFSCBitVectorProof::assignAlias(Expr expr) {
   static unsigned counter = 0;
-  Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end());
+  if (d_exprToVariableName.find(expr) != d_exprToVariableName.end()) {
+    return d_exprToVariableName[expr];
+  }
+
   std::stringstream ss;
   ss << "fbv" << counter++;
   Debug("pf::bv") << "assignAlias( " << expr << ") = " << ss.str() << std::endl;