summaryrefslogtreecommitdiff
path: root/src/theory/output_channel.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r--src/theory/output_channel.h4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 2c11097db..cc8cee481 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -19,6 +19,8 @@
#ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H
#define __CVC4__THEORY__OUTPUT_CHANNEL_H
+#include <memory>
+
#include "base/cvc4_assert.h"
#include "proof/proof_manager.h"
#include "smt/logic_exception.h"
@@ -97,7 +99,7 @@ class OutputChannel {
* @param pf - a proof of the conflict. This is only non-null if proofs
* are enabled.
*/
- virtual void conflict(TNode n, Proof* pf = nullptr) = 0;
+ virtual void conflict(TNode n, std::unique_ptr<Proof> pf = nullptr) = 0;
/**
* Propagate a theory literal.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback