summaryrefslogtreecommitdiff
path: root/src/proof/proof_manager.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/proof_manager.h')
-rw-r--r--src/proof/proof_manager.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 954b65bbc..b1cfc54b5 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -246,6 +246,7 @@ public:
assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
size_t size_unsat_core() const { return d_outputCoreFormulas.size(); }
+ bool unsatCoreAvailable() const;
void getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas);
int nextId() { return d_nextId++; }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback