From: Guy <katz911@gmail.com>
Date: Thu, 2 Jun 2016 17:17:14 +0000 (-0700)
Subject: Fix
X-Git-Tag: cvc5-1.0.0~6049^2~14
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9712043a682572bea37099168f2c161f597b0457;p=cvc5.git

Fix
---

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 479266db4..817444ca7 100644
--- 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;