From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 16 Aug 2013 21:07:22 +0000 (-0400)
Subject: Fix sat_proof "parentheses into the void" after conferring with Liana.
X-Git-Tag: cvc5-1.0.0~7287^2~14
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c46f66e6e50506f5e9c10df3dcb6db5affc45c78;p=cvc5.git

Fix sat_proof "parentheses into the void" after conferring with Liana.
---

diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 82478464f..d9b57f87e 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -595,7 +595,7 @@ void SatProof::markDeleted(CRef clause) {
 
 /// store mapping from theory atoms to new variables
 void SatProof::storeAtom(::Minisat::Lit literal, Expr atom) {
-  (d_atomToVar.find(atom) == d_atomToVar.end());
+  Assert(d_atomToVar.find(atom) == d_atomToVar.end());
   d_atomToVar[atom] = literal; 
 }