From: Tim King <taking@google.com>
Date: Tue, 29 Dec 2015 09:19:30 +0000 (-0500)
Subject: Adding a missing header include for cvc4_assert.h in smt_engine_check_proof.cpp for... 
X-Git-Tag: cvc5-1.0.0~6125
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1ce397129214a427a10ff3e33069e315fe13eec1;p=cvc5.git

Adding a missing header include for cvc4_assert.h in smt_engine_check_proof.cpp for when proofs are disabled.
---

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"