summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r--src/smt/smt_engine.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f898ee76a..5d8f31d3c 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -36,6 +36,7 @@
#include "util/result.h"
#include "util/sexpr.h"
#include "util/stats.h"
+#include "proof/proof_manager.h"
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
@@ -43,6 +44,7 @@
namespace CVC4 {
+
template <bool ref_count> class NodeTemplate;
typedef NodeTemplate<true> Node;
typedef NodeTemplate<false> TNode;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback