summaryrefslogtreecommitdiff
path: root/src/theory/theory_test_utils.h
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2017-11-15 02:58:30 -0800
committerAndres Noetzli <andres.noetzli@gmail.com>2017-11-15 02:58:30 -0800
commit3c130b44fdecc62b1ace2a739e77f913cd606aa0 (patch)
tree6abfb806dd45c83606c04dda5c26e9c410ac2ee1 /src/theory/theory_test_utils.h
parent85df7998e4362e0a9c796146d07d7b9e91045a31 (diff)
Adding garbage collection for Proof objects. (#1294)
Diffstat (limited to 'src/theory/theory_test_utils.h')
-rw-r--r--src/theory/theory_test_utils.h6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 4e0fd3e4d..8c2355cf4 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -20,6 +20,7 @@
#define __CVC4__THEORY__THEORY_TEST_UTILS_H
#include <iostream>
+#include <memory>
#include <utility>
#include <vector>
@@ -27,6 +28,7 @@
#include "expr/node.h"
#include "theory/interrupted.h"
#include "theory/output_channel.h"
+#include "util/proof.h"
#include "util/unsafe_interrupt_exception.h"
namespace CVC4 {
@@ -67,8 +69,8 @@ public:
~TestOutputChannel() override {}
void safePoint(uint64_t amount) override {}
-
- void conflict(TNode n, Proof* pf = nullptr) override {
+ void conflict(TNode n, std::unique_ptr<Proof> pf) override
+ {
push(CONFLICT, n);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback