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<stdio.h>
-#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() {