From: guykatzz <katz911@gmail.com>
Date: Thu, 4 May 2017 20:51:36 +0000 (-0700)
Subject: skolemization manager may be called also when just unsatCores are on (related to... 
X-Git-Tag: cvc5-1.0.0~5811
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b8d1e24fb00ca15dc523ec45d791473c1e5b8756;p=cvc5.git

skolemization manager may be called also when just unsatCores are on (related to bug 717)
---

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index cbc7f591a..2bab09789 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -135,7 +135,7 @@ ArithProof* ProofManager::getArithProof() {
 }
 
 SkolemizationManager* ProofManager::getSkolemizationManager() {
-  Assert (options::proof());
+  Assert (options::proof() || options::unsatCores());
   return &(currentPM()->d_skolemizationManager);
 }