diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp
index 211e2abde..fd7c94f22 100644
--- a/src/api/api_config_params.cpp
+++ b/src/api/api_config_params.cpp
@@ -46,16 +46,14 @@ extern "C" {
         gparams::reset();
         env_params::updt_params();
     }
-
-    static std::string g_Z3_global_param_get_buffer;
     
     Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
         memory::initialize(UINT_MAX);
         LOG_Z3_global_param_get(param_id, param_value);
         *param_value = nullptr;
         try {
-            g_Z3_global_param_get_buffer = gparams::get_value(param_id);
-            *param_value = g_Z3_global_param_get_buffer.c_str();
+            gparams::g_buffer() = gparams::get_value(param_id);
+            *param_value = gparams::g_buffer().c_str();
             return true;
         }
         catch (z3_exception & ex) {
diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h
index 6b1f02ca1..49767274d 100644
--- a/src/math/lp/var_register.h
+++ b/src/math/lp/var_register.h
@@ -39,7 +39,7 @@ public:
 };
 
 class var_register {
-    svector<ext_var_info> m_local_to_external;
+    vector<ext_var_info> m_local_to_external;
     std::unordered_map<unsigned, unsigned> m_external_to_local;
     unsigned m_locals_mask;
     unsigned m_locals_mask_inverted;
diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp
index abf8e5625..941b1e0ac 100644
--- a/src/sat/smt/euf_ackerman.cpp
+++ b/src/sat/smt/euf_ackerman.cpp
@@ -34,6 +34,7 @@ namespace euf {
             m.dec_ref(inf->a);
             m.dec_ref(inf->b);
             m.dec_ref(inf->c);
+            dealloc(inf);
         }
         m_table.reset();
         m_queue = nullptr;        
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index ce8083cc2..73eee2ad1 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -46,7 +46,6 @@ Revision History:
 
 typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_MPS, IN_DRAT } input_kind;
 
-static std::string  g_aux_input_file;
 static char const * g_input_file          = nullptr;
 static char const * g_drat_input_file     = nullptr;
 static bool         g_standard_input      = false;
@@ -124,7 +123,7 @@ void display_usage() {
     std::cout << "Use 'z3 -p' for the complete list of global and module parameters.\n";
 }
    
-static void parse_cmd_line_args(int argc, char ** argv) {
+static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv) {
     long timeout = 0;
     int i = 1;
     char * eq_pos = nullptr;
@@ -134,19 +133,18 @@ static void parse_cmd_line_args(int argc, char ** argv) {
         if (arg[0] == '-' && arg[1] == '-' && arg[2] == 0) {
             // Little hack used to read files with strange names such as -foo.smt2
             // z3 -- -foo.smt2
-            i++;
-            g_aux_input_file = "";
-            for (; i < argc; i++) {
-                g_aux_input_file += argv[i];
-                if (i < argc - 1)
-                    g_aux_input_file += " ";
-            }
             if (g_input_file) {
                 warning_msg("input file was already specified.");
+                break;
             }
-            else {
-                g_input_file = g_aux_input_file.c_str();
+            i++;
+            input_file = "";
+            for (; i < argc; i++) {
+                input_file += argv[i];
+                if (i < argc - 1)
+                    input_file += " ";
             }
+            g_input_file = input_file.c_str();
             break;
         }
         
@@ -321,11 +319,12 @@ static void parse_cmd_line_args(int argc, char ** argv) {
 
 
 int STD_CALL main(int argc, char ** argv) {
-     try{
+     try {
         unsigned return_value = 0;
         memory::initialize(0);
         memory::exit_when_out_of_memory(true, "ERROR: out of memory");
-        parse_cmd_line_args(argc, argv);
+        std::string input_file;
+        parse_cmd_line_args(input_file, argc, argv);
         env_params::updt_params();
 
         if (g_input_file && g_standard_input) {
diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
index d227bced5..0c679e388 100644
--- a/src/util/gparams.cpp
+++ b/src/util/gparams.cpp
@@ -137,6 +137,7 @@ struct gparams::imp {
     smap<params_ref* >   m_module_params;
     params_ref           m_params;
     region               m_region;
+    std::string          m_buffer;
 
     void check_registered() {
         if (m_modules_registered)
@@ -651,3 +652,8 @@ void gparams::finalize() {
     dealloc(g_imp);
     DEALLOC_MUTEX(gparams_mux);
 }
+
+std::string& gparams::g_buffer() {
+    SASSERT(g_imp);
+    return g_imp->m_buffer;
+}
diff --git a/src/util/gparams.h b/src/util/gparams.h
index 75e8cb02c..0efad4a07 100644
--- a/src/util/gparams.h
+++ b/src/util/gparams.h
@@ -26,6 +26,9 @@ class gparams {
 public:
     typedef default_exception exception;
 
+    static std::string& g_buffer();
+
+
     /**
        \brief Reset all global and module parameters.
     */
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index 644c234c4..e144cf636 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -153,4 +153,5 @@ void scoped_timer::finalize() {
         }
     }
     num_workers = 0;
+    available_workers.clear();
 }