From ca97bfb4b80b03dec103afabccc4aa155c88673e Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 5 Jul 2020 11:44:12 +0100 Subject: [PATCH] fix build --- src/api/z3_api.h | 6 +++--- src/smt/smt_enode.h | 4 ++-- src/util/mpq_inf.h | 10 +++++----- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ac7f899ef..f8448a81b 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -2,7 +2,7 @@ Copyright (c) 2015 Microsoft Corporation --*/ -#ifndef Z3_API_H_ +#pragma once DEFINE_TYPE(Z3_symbol); DEFINE_TYPE(Z3_literals); @@ -5557,12 +5557,12 @@ extern "C" { */ Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str); - + /*@}*/ /** @name Error Handling */ /*@{*/ -#pragma once +#ifndef SAFE_ERRORS /** \brief Return the error code for the last API call. diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 6e2796dc1..7047c97c4 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -16,7 +16,7 @@ Author: Revision History: --*/ -#ifndef SMT_ENODE_H_ +#pragma once #include "ast/ast.h" #include "smt/smt_types.h" @@ -46,7 +46,7 @@ namespace smt { // #define SPARSE_MAP -#pragma once +#ifndef SPARSE_MAP typedef ptr_vector app2enode_t; // app -> enode #else class app2enode_t : public u_map { diff --git a/src/util/mpq_inf.h b/src/util/mpq_inf.h index 16d3da866..e2bcbcba6 100644 --- a/src/util/mpq_inf.h +++ b/src/util/mpq_inf.h @@ -16,7 +16,7 @@ Author: Revision History: --*/ -#ifndef MPQ_INF_H_ +#pragma once #include "util/mpq.h" #include "util/hash.h" @@ -39,14 +39,14 @@ public: } enum inf_kind { NEG=-1, ZERO, POS }; - + void reset(mpq_inf & a) { m.reset(a.first); m.reset(a.second); } - + unsigned hash(mpq_inf const & a) const { return hash_u_u(m.hash(a.first), m.hash(a.second)); } - + void del(mpq_inf & a) { m.del(a.first); m.del(a.second); @@ -278,7 +278,7 @@ public: mpq_manager& get_mpq_manager() { return m; } }; -#pragma once +#ifndef SINGLE_THREAD typedef mpq_inf_manager synch_mpq_inf_manager; #else typedef mpq_inf_manager synch_mpq_inf_manager;