summaryrefslogtreecommitdiff
path: root/src/include/prover.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/include/prover.h')
-rw-r--r--src/include/prover.h5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/include/prover.h b/src/include/prover.h
index 7abfafe63..e48d6336c 100644
--- a/src/include/prover.h
+++ b/src/include/prover.h
@@ -10,6 +10,11 @@
#ifndef __CVC4_PROVER_H
#define __CVC4_PROVER_H
+#include <vector>
+#include "expr.h"
+#include "result.h"
+#include "model.h"
+
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
// PropEngine.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback