summaryrefslogtreecommitdiff
path: root/src/proof
diff options
context:
space:
mode:
authorguykatzz <katz911@gmail.com>2017-05-04 13:51:36 -0700
committerguykatzz <katz911@gmail.com>2017-05-04 13:51:36 -0700
commitb8d1e24fb00ca15dc523ec45d791473c1e5b8756 (patch)
tree7f5533f40bbaed0a62ea44fcdddf9e0763954341 /src/proof
parent2a3df5f6297e9a95abb9ba093f21e70eec3773b8 (diff)
skolemization manager may be called also when just unsatCores are on (related to bug 717)
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/proof_manager.cpp2
1 files changed, 1 insertions, 1 deletions
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback