From 1ce397129214a427a10ff3e33069e315fe13eec1 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 29 Dec 2015 04:19:30 -0500 Subject: [PATCH] Adding a missing header include for cvc4_assert.h in smt_engine_check_proof.cpp for when proofs are disabled. --- src/smt/smt_engine_check_proof.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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 #include -#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" -- 2.30.2