From 5cda9504f1e4a9aae49a3e657a31b82e492510fb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 Jul 2017 16:32:26 -0700 Subject: [PATCH] remove relative include from API Signed-off-by: Nikolaj Bjorner --- src/api/z3.h | 20 ++++++++++---------- src/smt/smt_setup.cpp | 7 ++++++- 2 files changed, 16 insertions(+), 11 deletions(-) diff --git a/src/api/z3.h b/src/api/z3.h index 22a1b9b5d..c9f0fe6e2 100644 --- a/src/api/z3.h +++ b/src/api/z3.h @@ -22,16 +22,16 @@ Notes: #define Z3_H_ #include -#include "api/z3_macros.h" -#include "api/z3_api.h" -#include "api/z3_ast_containers.h" -#include "api/z3_algebraic.h" -#include "api/z3_polynomial.h" -#include "api/z3_rcf.h" -#include "api/z3_fixedpoint.h" -#include "api/z3_optimization.h" -#include "api/z3_interp.h" -#include "api/z3_fpa.h" +#include "z3_macros.h" +#include "z3_api.h" +#include "z3_ast_containers.h" +#include "z3_algebraic.h" +#include "z3_polynomial.h" +#include "z3_rcf.h" +#include "z3_fixedpoint.h" +#include "z3_optimization.h" +#include "z3_interp.h" +#include "z3_fpa.h" #endif diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 361448316..1be1bca17 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -720,7 +720,12 @@ namespace smt { } void setup::setup_i_arith() { - m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); + if (m_params.m_arith_mode == AS_OPTINF) { + m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params)); + } + else { + m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); + } } void setup::setup_r_arith() {