summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
authorTim King <taking@google.com>2015-12-29 04:19:30 -0500
committerTim King <taking@google.com>2015-12-29 04:20:09 -0500
commit1ce397129214a427a10ff3e33069e315fe13eec1 (patch)
tree3bde88f454318a3457bcefcbccb54f0333becbe4 /src/smt
parent815f2c96856e96e977b725254b65d68fc0323947 (diff)
Adding a missing header include for cvc4_assert.h in smt_engine_check_proof.cpp for when proofs are disabled.
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/smt_engine_check_proof.cpp5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index 2add88afb..da01b9863 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -22,8 +22,11 @@
#include <fstream>
#include <string>
-#include "base/output.h"
+#warning "TODO: Why is lfsc's check.h being included like this?"
#include "check.h"
+
+#include "base/cvc4_assert.h"
+#include "base/output.h"
#include "expr/statistics_registry.h"
#include "smt/smt_engine.h"
#include "util/configuration_private.h"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback