diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index cfe082802..31535e5f4 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -989,7 +989,7 @@ extern "C" {
             case OP_TO_INT: return Z3_OP_TO_INT;
             case OP_IS_INT: return Z3_OP_IS_INT;
             default:
-                UNREACHABLE();
+                //UNREACHABLE();
                 return Z3_OP_UNINTERPRETED;
             }
         }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 55b61d0da..5f9de116d 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -546,6 +546,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
         s == "QF_FPBV" ||
         s == "QF_BVFP" ||
         s == "QF_S" ||
+        s == "ALL" ||
         s == "HORN";
 }
 
@@ -566,6 +567,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
         s == "QF_BVRE" ||
         s == "QF_FPBV" ||
         s == "QF_BVFP" ||
+        s == "ALL" ||
         s == "HORN";
 }
 
@@ -609,6 +611,7 @@ bool cmd_context::logic_has_array_core(symbol const & s) const {
         s == "AUFNIRA" ||
         s == "AUFBV" ||
         s == "ABV" ||
+        s == "ALL" ||
         s == "QF_ABV" ||
         s == "QF_AUFBV" ||
         s == "HORN";
@@ -702,7 +705,7 @@ void cmd_context::init_external_manager() {
 }
 
 bool cmd_context::supported_logic(symbol const & s) const {
-    return s == "QF_UF" || s == "UF" ||
+    return s == "QF_UF" || s == "UF" || 
         logic_has_arith_core(s) || logic_has_bv_core(s) ||
         logic_has_array_core(s) || logic_has_seq_core(s) ||
         logic_has_horn(s) || logic_has_fpa_core(s);
diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index 85fbbdb3a..424b95359 100755
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -45,7 +45,6 @@
 #include"scoped_ctrl_c.h"
 #include"cancel_eh.h"
 #include"scoped_timer.h"
-//#  include"pp_params.hpp"
 
 /* A wrapper around an ast manager, providing convenience methods. */