diff --git a/src/Makefile b/src/Makefile
index 445c6ff7b..9a14fc6ba 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -276,6 +276,7 @@ core_src_c := \
 	utils/csets.c \
 	utils/cputime.c \
 	utils/dep_tables.c \
+	utils/error.c \
 	utils/gcd.c \
 	utils/generic_heap.c \
 	utils/hash_functions.c \
@@ -494,7 +495,6 @@ bin_src_c := \
 	frontend/yices_sat_new.c \
 	frontend/yices_smt.c \
 	frontend/yices_smt2.c \
-	frontend/yices_smt2_mt.c \
 	frontend/yices_smtcomp.c \
 
 #
diff --git a/src/api/yices_api.c b/src/api/yices_api.c
index 47f1dd452..faed13510 100644
--- a/src/api/yices_api.c
+++ b/src/api/yices_api.c
@@ -1108,6 +1108,11 @@ EXPORTED void yices_exit(void) {
     delete_sparse_array(&the_root_types);
   }
 
+  free_parameter_list();
+  free_config_list();
+  free_model_list();
+  free_context_list();
+
   delete_parsing_objects();
   delete_fvars();
 
@@ -1123,11 +1128,6 @@ EXPORTED void yices_exit(void) {
   free_bvarith64_buffer_list();
   free_arith_buffer_list();
 
-  free_context_list();
-  free_model_list();
-  free_config_list();
-  free_parameter_list();
-
   delete_list_locks();
 
   q_clear(&r0);
diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c
index 4d27ed7ba..af6483f4f 100644
--- a/src/frontend/smt2/smt2_commands.c
+++ b/src/frontend/smt2/smt2_commands.c
@@ -2653,8 +2653,13 @@ static void init_search_parameters(smt2_globals_t *g) {
 static void timeout_handler(void *data) {
   smt2_globals_t *g;
 
+#ifndef THREAD_SAFE
   assert(data == &__smt2_globals);
-
+#else
+  /* In the multi-threaded case there are multiple copies of the
+     global data. */
+#endif /* THREAD_SAFE */
+  
   g = data;
   if (g->efmode && g->ef_client.efsolver != NULL && g->ef_client.efsolver->status == EF_STATUS_SEARCHING) {
     ef_solver_stop_search(g->ef_client.efsolver);
@@ -2679,14 +2684,13 @@ static smt_status_t check_sat_with_timeout(smt2_globals_t *g, const param_t *par
    * We call init_timeout only now because the internal timeout
    * consumes resources even if it's never used.
    */
-  if (! g->timeout_initialized) {
-    init_timeout();
-    g->timeout_initialized = true;
+  if (! g->to) {
+    g->to = init_timeout();
   }
   g->interrupted = false;
-  start_timeout(g->timeout, timeout_handler, g);
+  start_timeout(g->to, g->timeout, timeout_handler, g);
   stat = check_context(g->ctx, params);
-  clear_timeout();
+  clear_timeout(g->to);
 
   /*
    * Attempt to cleanly recover from interrupt
@@ -2725,15 +2729,14 @@ static smt_status_t check_sat_with_assumptions(smt2_globals_t *g, const param_t
    * We call init_timeout only now because the internal timeout
    * consumes resources even if it's never used.
    */
-  if (! g->timeout_initialized) {
-    init_timeout();
-    g->timeout_initialized = true;
+  if (! g->to) {
+    g->to = init_timeout();
   }
   g->interrupted = false;
-  start_timeout(g->timeout, timeout_handler, g);
+  start_timeout(g->to, g->timeout, timeout_handler, g);
   stat = check_with_assumptions(g->ctx, params, a->assumptions.size, a->assumptions.data, &a->core);
   a->status = stat;
-  clear_timeout();
+  clear_timeout(g->to);
 
   /*
    * Attempt to cleanly recover from interrupt
@@ -2773,14 +2776,13 @@ static smt_status_t check_sat_with_model(smt2_globals_t *g, const param_t *param
    * We call init_timeout only now because the internal timeout
    * consumes resources even if it's never used.
    */
-  if (! g->timeout_initialized) {
-    init_timeout();
-    g->timeout_initialized = true;
+  if (! g->to) {
+    g->to = init_timeout();
   }
   g->interrupted = false;
-  start_timeout(g->timeout, timeout_handler, g);
+  start_timeout(g->to, g->timeout, timeout_handler, g);
   stat = check_with_model(g->ctx, params, n, vars, values);
-  clear_timeout();
+  clear_timeout(g->to);
 
   /*
    * Attempt to cleanly recover from interrupt
@@ -3026,7 +3028,7 @@ static void add_delayed_assertion(smt2_globals_t *g, term_t t) {
 /*
  * Check satisfiability of all assertions
  */
-static void check_delayed_assertions(smt2_globals_t *g) {
+static void check_delayed_assertions(smt2_globals_t *g, bool report) {
   int32_t code;
   smt_status_t status;
   model_t *model;
@@ -3036,12 +3038,14 @@ static void check_delayed_assertions(smt2_globals_t *g) {
 
   if (g->trivially_unsat) {
     trace_printf(g->tracer, 3, "(check-sat: trivially unsat)\n");
-    report_status(g, STATUS_UNSAT);
+    if (report)
+      report_status(g, STATUS_UNSAT);
   } else if (trivially_true_assertions(g->assertions.data, g->assertions.size, &model)) {
     trace_printf(g->tracer, 3, "(check-sat: trivially true)\n");
     g->trivially_sat = true;
     g->model = model;
-    report_status(g, STATUS_SAT);
+    if (report)
+      report_status(g, STATUS_SAT);
   } else {
     /*
      * check for mislabeled benchmarks: some benchmarks
@@ -3105,7 +3109,8 @@ static void check_delayed_assertions(smt2_globals_t *g) {
 	status = check_sat_with_timeout(g, &g->parameters);
       }
 
-      report_status(g, status);
+      if (report)
+	report_status(g, status);
     }
   }
 }
@@ -3312,18 +3317,17 @@ static void efsolve_cmd(smt2_globals_t *g) {
   if (g->efmode) {
     efc = &g->ef_client;
     if (g->timeout != 0) {
-      if (! g->timeout_initialized) {
-        init_timeout();
-        g->timeout_initialized = true;
+      if (! g->to) {
+        g->to = init_timeout();
       }
       g->interrupted = false;
-      start_timeout(g->timeout, timeout_handler, g);
+      start_timeout(g->to, g->timeout, timeout_handler, g);
     }
 
     ef_solve(efc, g->assertions.size, g->assertions.data, &g->parameters,
 	     qf_fragment(g->logic_code), ef_arch_for_logic(g->logic_code),
              g->tracer, &g->term_patterns);
-    if (g-> timeout != 0) clear_timeout();
+    if (g-> timeout != 0) clear_timeout(g->to);
 
     if (efc->efcode != EF_NO_ERROR) {
       // error in preprocessing
@@ -4577,7 +4581,7 @@ static void init_smt2_globals(smt2_globals_t *g) {
   init_params_to_defaults(&g->parameters);
   g->nthreads = 0;
   g->timeout = 0;
-  g->timeout_initialized = false;
+  g->to = NULL;
   g->interrupted = false;
   g->delegate = NULL;
   g->avtbl = NULL;
@@ -4629,8 +4633,8 @@ static void init_smt2_globals(smt2_globals_t *g) {
  * - delete the timeout object if it's initialized
  */
 static void delete_smt2_globals(smt2_globals_t *g) {
-  if (g->timeout_initialized) {
-    delete_timeout();
+  if (g->to) {
+    delete_timeout(g->to);
   }
   delete_info_table(g);
   if (g->logic_name != NULL) {
@@ -6598,7 +6602,7 @@ static yices_thread_result_t YICES_THREAD_ATTR check_delayed_assertions_thread(v
   g->out = output;   // /tmp/check_delayed_assertions_thread_<thread index>.txt
   g->err = output;   // /tmp/check_delayed_assertions_thread_<thread index>.txt
 
-  check_delayed_assertions(g);
+  check_delayed_assertions(g, /*report=*/false);
 
   return yices_thread_exit();
 }
@@ -6621,18 +6625,22 @@ static smt_status_t get_status_from_globals(smt2_globals_t *g) {
 static void check_delayed_assertions_mt(smt2_globals_t *g) {
   bool success;
   uint32_t i, n;
+  bool verbose;
 
   n = g->nthreads;
   assert(n > 0);
 
+  verbose = g->verbosity > 0;
+    
   smt2_globals_t *garray =  (smt2_globals_t *) safe_malloc(n * sizeof(smt2_globals_t));
   for(i = 0; i < n; i++) {
     garray[i] = __smt2_globals;  // just copy them for now.
     garray[i].tracer = NULL;     // only main thread can use this.
   }
-  launch_threads(n, garray, sizeof(smt2_globals_t), "check_delayed_assertions_thread", check_delayed_assertions_thread, true);
-  fprintf(stderr, "All threads finished. Now computing check_delayed_assertions in main thread.\n");
-  check_delayed_assertions(g);
+  launch_threads(n, garray, sizeof(smt2_globals_t), "check_delayed_assertions_thread", check_delayed_assertions_thread, verbose);
+  if (verbose)
+    fprintf(stderr, "All threads finished. Now computing check_delayed_assertions in main thread.\n");
+  check_delayed_assertions(g, /*report=*/true);
 
   //could check that they are all OK
 
@@ -6646,11 +6654,9 @@ static void check_delayed_assertions_mt(smt2_globals_t *g) {
     //free the model if there is one, and free the context.
     //IAM: valgrind says there is no leak here. This is puzzling.
   }
-  if (success) {
-    fprintf(stderr, "SUCCESS: All threads agree.\n");
-  } else {
-    fprintf(stderr, "FAILURE: Threads disagree.\n");
-  }
+  if (verbose)
+    fprintf(stderr,
+	    success ? "SUCCESS: All threads agree.\n" : "FAILURE: Threads disagree.\n");
   safe_free(garray);
 }
 #endif
@@ -6679,10 +6685,10 @@ void smt2_check_sat(void) {
       } else {
 	//	show_delayed_assertions(&__smt2_globals);
 #ifndef THREAD_SAFE
-        check_delayed_assertions(&__smt2_globals);
+        check_delayed_assertions(&__smt2_globals, /*report=*/true);
 #else
         if (__smt2_globals.nthreads == 0) {
-          check_delayed_assertions(&__smt2_globals);
+          check_delayed_assertions(&__smt2_globals, /*report=*/true);
         } else {
 	  check_delayed_assertions_mt(&__smt2_globals);
 	}
diff --git a/src/frontend/smt2/smt2_commands.h b/src/frontend/smt2/smt2_commands.h
index e673bee13..c7d45ef72 100644
--- a/src/frontend/smt2/smt2_commands.h
+++ b/src/frontend/smt2/smt2_commands.h
@@ -50,6 +50,7 @@
 #include "utils/int_vectors.h"
 #include "utils/ptr_vectors.h"
 #include "utils/string_hash_map.h"
+#include "utils/timeout.h"
 #include "parser_utils/lexer.h"
 #include "parser_utils/term_stack2.h"
 #include "io/tracer.h"
@@ -401,7 +402,7 @@ typedef struct smt2_globals_s {
 
   // timeout
   uint32_t timeout;           // default = 0 (no timeout)
-  bool timeout_initialized;   // initially false. true once init_timeout is called
+  timeout_t *to;              // initially NULL. Non-NULL once init_timeout is called
   bool interrupted;           // true if the most recent call to check_sat timed out
 
   // optional: delegate sat solver for QF_BV
diff --git a/src/frontend/yices/yices_reval.c b/src/frontend/yices/yices_reval.c
index 14a0bb7b5..d1c8bd47a 100644
--- a/src/frontend/yices/yices_reval.c
+++ b/src/frontend/yices/yices_reval.c
@@ -138,7 +138,7 @@
  * OTHER
  * - timeout: timeout value in second (applies to check)
  *   timeout value = 0 means no timeout
- * - timeout_initialized: true once init_timeout is called
+ * - to: the timeout structure
  *
  * COMMAND-LINE OPTIONS:
  * - logic_name: logic to use (option --logic=xxx)
@@ -175,7 +175,7 @@ static int32_t verbosity;
 static tracer_t *tracer;
 
 static uint32_t timeout;
-static bool timeout_initialized;
+static timeout_t *to;
 
 static char *logic_name;
 static char *arith_name;
@@ -262,8 +262,6 @@ static pp_area_t pp_area = {
   140, UINT32_MAX, 0, false, false
 };
 
-
-
 /**************************
  *  COMMAND-LINE OPTIONS  *
  *************************/
@@ -2542,11 +2540,10 @@ static void timeout_handler(void *data) {
  */
 static void set_timeout(void) {
   if (timeout > 0) {
-    if (!timeout_initialized) {
-      init_timeout();
-      timeout_initialized = true;
+    if (!to) {
+      to = init_timeout();
     }
-    start_timeout(timeout, timeout_handler, context);
+    start_timeout(to, timeout, timeout_handler, context);
   }
 }
 
@@ -2555,8 +2552,8 @@ static void set_timeout(void) {
  */
 static void reset_timeout(void) {
   if (timeout > 0) {
-    assert(timeout_initialized);
-    clear_timeout();
+    assert(to);
+    clear_timeout(to);
     timeout = 0;
   }
 }
@@ -3999,7 +3996,7 @@ int yices_main(int argc, char *argv[]) {
    */
   interactive = false;
   timeout = 0;
-  timeout_initialized = false;
+  to = NULL;
   include_depth = 0;
   ready_time = 0.0;
   check_process_time = 0.0;
@@ -4111,8 +4108,8 @@ int yices_main(int argc, char *argv[]) {
 
   yices_exit();
 
-  if (timeout_initialized) {
-    delete_timeout();
+  if (to) {
+    delete_timeout(to);
   }
 
   return exit_code;
diff --git a/src/frontend/yices_smt.c b/src/frontend/yices_smt.c
index e70a3b7fc..8c9236871 100644
--- a/src/frontend/yices_smt.c
+++ b/src/frontend/yices_smt.c
@@ -182,6 +182,7 @@ static arith_solver_t arith_solver;
  */
 static uint32_t timeout;
 
+static timeout_t *to;
 
 /*
  * Filename given on the command line
@@ -2040,15 +2041,15 @@ static int process_benchmark(char *filename) {
     start_search_time = get_cpu_time();
 
     if (timeout > 0) {
-      init_timeout();
-      start_timeout(timeout, timeout_handler, &context);
+      to = init_timeout();
+      start_timeout(to, timeout, timeout_handler, &context);
     }
     code = check_context(&context, search_options);
     clear_handler();
 
     if (timeout > 0) {
-      clear_timeout();
-      delete_timeout();
+      clear_timeout(to);
+      delete_timeout(to);
     }
 
     print_results();
diff --git a/src/frontend/yices_smt2.c b/src/frontend/yices_smt2.c
index f7fd78344..e7d9232f8 100644
--- a/src/frontend/yices_smt2.c
+++ b/src/frontend/yices_smt2.c
@@ -140,6 +140,7 @@ static double ef_ematch_term_alpha;
 static int32_t ef_ematch_cnstr_mode;
 static int32_t ef_ematch_term_mode;
 
+static uint32_t nthreads;
 
 /****************************
  *  COMMAND-LINE ARGUMENTS  *
@@ -185,9 +186,10 @@ typedef enum optid {
   ematch_term_alpha_opt,            // set ematch term learner learning rate
   ematch_cnstr_mode_opt,            // set cnstr mode in ematching
   ematch_term_mode_opt,             // set term mode in ematching
+  nthreads_opt,                     // number of threads
 } optid_t;
 
-#define NUM_OPTIONS (ematch_term_mode_opt+1)
+#define NUM_OPTIONS (nthreads_opt+1)
 
 /*
  * Option descriptors
@@ -232,6 +234,7 @@ static option_desc_t options[NUM_OPTIONS] = {
   { "ematch-term-alpha", '\0', MANDATORY_FLOAT, ematch_term_alpha_opt },
   { "ematch-cnstr-mode", '\0', MANDATORY_STRING, ematch_cnstr_mode_opt },
   { "ematch-term-mode", '\0', MANDATORY_STRING, ematch_term_mode_opt },
+  { "nthreads", 'n', MANDATORY_INT, nthreads_opt }
 };
 
 
@@ -271,6 +274,8 @@ static void print_help(const char *progname) {
          "    --mcsat                   Use the MCSat solver\n"
          "    --mcsat-help              Show the MCSat options\n"
          "    --ef-help                 Show the EF options\n"
+	 "    --nthreads=<number of threads>  Specify the number of threads (default = 0 = main thread only)\n"
+	 "    -n <number of threads>\n"
          "\n"
          "For bug reports and other information, please see http://yices.csl.sri.com/\n");
   fflush(stdout);
@@ -406,6 +411,8 @@ static void parse_command_line(int argc, char *argv[]) {
   ef_ematch_cnstr_mode = -1;
   ef_ematch_term_mode = -1;
 
+  nthreads = 0;
+
   init_cmdline_parser(&parser, options, NUM_OPTIONS, argv, argc);
 
   for (;;) {
@@ -463,6 +470,17 @@ static void parse_command_line(int argc, char *argv[]) {
         timeout = v;
         break;
 
+      case nthreads_opt:
+	v = elem.i_value;
+	if (v < 0) {
+	  fprintf(stderr, "%s: the number of threads must be non-negative\n", parser.command_name);
+	  print_usage(parser.command_name);
+	  code = YICES_EXIT_USAGE;
+	  goto exit;
+	}
+	nthreads = v;
+	break;
+	
       case incremental_opt:
         incremental = true;
         break;
@@ -1059,7 +1077,7 @@ int main(int argc, char *argv[]) {
   init_handlers();
 
   yices_init();
-  init_smt2(!incremental, timeout, interactive);
+  init_mt2(!incremental, timeout, nthreads, interactive);
   if (smt2_model_format) smt2_force_smt2_model_format();
   if (bvdecimal) smt2_force_bvdecimal_format();
   if (dimacsfile != NULL && delegate == NULL) smt2_export_to_dimacs(dimacsfile);
diff --git a/src/frontend/yices_smt2_mt.c b/src/frontend/yices_smt2_mt.c
deleted file mode 100644
index 255429629..000000000
--- a/src/frontend/yices_smt2_mt.c
+++ /dev/null
@@ -1,638 +0,0 @@
-/*
- * This file is part of the Yices SMT Solver.
- * Copyright (C) 2017 SRI International.
- *
- * Yices is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * Yices is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
- */
-
-/*
- * Yices solver: input in the SMT-LIB 2.0 language multithreaded test bed
- */
-
-#if defined(CYGWIN) || defined(MINGW)
-#ifndef __YICES_DLLSPEC__
-#define __YICES_DLLSPEC__ __declspec(dllexport)
-#endif
-#endif
-
-#include <stdio.h>
-#include <stdlib.h>
-#include <stdbool.h>
-#include <signal.h>
-#include <errno.h>
-#include <unistd.h>
-#include <inttypes.h>
-// EXPERIMENT
-#include <locale.h>
-
-
-#include "frontend/common/parameters.h"
-#include "frontend/smt2/smt2_commands.h"
-#include "frontend/smt2/smt2_lexer.h"
-#include "frontend/smt2/smt2_parser.h"
-#include "frontend/smt2/smt2_term_stack.h"
-#include "utils/command_line.h"
-
-#include "yices.h"
-#include "yices_exit_codes.h"
-
-/*
- * yices_rev is set up at compile time in yices_version.c
- */
-extern const char * const yices_rev;
-
-/*
- * Global objects:
- * - lexer/parser/stack: for processing the SMT2 input
- * - incremental: if this flag is true, support for push/pop
- *   and multiple check_sat is enabled. Otherwise, the solver
- *   is configured to handle a set of declarations/assertions
- *   followed by a single call to (check_sat).
- * - interactive: if this flag is true, print a prompt before
- *   parsing commands. Also set the option :print-success to true.
- * - timeout: command-line option
- *
- * - filename = name of the input file (NULL means read stdin)
- */
-static lexer_t lexer;
-static parser_t parser;
-static tstack_t stack;
-
-static bool incremental;
-static bool interactive;
-static bool show_stats;
-static int32_t verbosity;
-static uint32_t timeout;
-static uint32_t nthreads;
-static char *filename;
-
-// mcsat options
-static bool mcsat;
-static bool mcsat_nra_mgcd;
-static bool mcsat_nra_nlsat;
-static bool mcsat_nra_bound;
-static int32_t mcsat_nra_bound_min;
-static int32_t mcsat_nra_bound_max;
-
-static pvector_t trace_tags;
-
-
-/****************************
- *  COMMAND-LINE ARGUMENTS  *
- ***************************/
-
-typedef enum optid {
-  show_version_opt,        // print version and exit
-  show_help_opt,           // print help and exit
-  show_stats_opt,          // show statistics after all commands are processed
-  verbosity_opt,           // set verbosity on the command line
-  incremental_opt,         // enable incremental mode
-  interactive_opt,         // enable interactive mode
-  timeout_opt,             // give a timeout
-  nthreads_opt,            // number of threads
-  mcsat_opt,               // enable mcsat
-  mcsat_nra_mgcd_opt,      // use the mgcd instead psc in projection
-  mcsat_nra_nlsat_opt,     // use the nlsat projection instead of brown single-cell
-  mcsat_nra_bound_opt,     // search by increasing bound
-  mcsat_nra_bound_min_opt, // set initial bound
-  mcsat_nra_bound_max_opt, // set maximal bound
-  trace_opt,               // enable a trace tag
-} optid_t;
-
-#define NUM_OPTIONS (trace_opt+1)
-
-/*
- * Option descriptors
- */
-static option_desc_t options[NUM_OPTIONS] = {
-  { "version", 'V', FLAG_OPTION, show_version_opt },
-  { "help", 'h', FLAG_OPTION, show_help_opt },
-  { "stats", 's', FLAG_OPTION, show_stats_opt },
-  { "verbosity", 'v', MANDATORY_INT, verbosity_opt },
-  { "timeout", 't', MANDATORY_INT, timeout_opt },
-  { "nthreads", 'n', MANDATORY_INT, nthreads_opt },
-  { "incremental", '\0', FLAG_OPTION, incremental_opt },
-  { "interactive", '\0', FLAG_OPTION, interactive_opt },
-  { "mcsat", '\0', FLAG_OPTION, mcsat_opt },
-  { "mcsat-nra-mgcd", '\0', FLAG_OPTION, mcsat_nra_mgcd_opt },
-  { "mcsat-nra-nlsat", '\0', FLAG_OPTION, mcsat_nra_nlsat_opt },
-  { "mcsat-nra-bound", '\0', FLAG_OPTION, mcsat_nra_bound_opt },
-  { "mcsat-nra-bound-min", '\0', MANDATORY_INT, mcsat_nra_bound_min_opt },
-  { "mcsat-nra-bound-max", '\0', MANDATORY_INT, mcsat_nra_bound_max_opt },
-  { "trace", 't', MANDATORY_STRING, trace_opt },
-};
-
-
-/*
- * Processing of command-line
- */
-static void print_version(void) {
-  printf("Yices %s\n"
-	 "Copyright SRI International.\n"
-         "Linked with GMP %s\n"
-	 "Copyright Free Software Foundation, Inc.\n"
-         "Build date: %s\n"
-         "Platform: %s (%s)\n"
-         "Revision: %s\n",
-         yices_version, gmp_version,
-         yices_build_date, yices_build_arch, yices_build_mode, yices_rev);
-  fflush(stdout);
-}
-
-static void print_help(const char *progname) {
-  printf("Usage: %s [option] filename\n"
-         "    or %s [option]\n", progname, progname);
-  printf("Option summary:\n"
-	 "    --version, -V             Show version and exit\n"
-	 "    --help, -h                Print this message and exit\n"
-	 "    --verbosity=<level>       Set verbosity level (default = 0)\n"
-	 "             -v <level>\n"
-	 "    --timeout=<timeout>       Set a timeout in seconds (default = no timeout)\n"
-	 "           -t <timeout>\n"
-	 "    --nthreads=<number of threads>  Specify the number of threads (default = 0 = main thread only)\n"
-	 "           -n <number of threads>\n"
-	 "    --stats, -s               Print statistics once all commands have been processed\n"
-	 "    --incremental             Enable support for push/pop\n"
-	 "    --interactive             Run in interactive mode (ignored if a filename is given)\n"
-#if HAVE_MCSAT
-   "    --mcsat                   Use the MCSat solver\n"
-   "    --mcsat-nra-mgcd          Use model-based GCD instead of PSC for projection\n"
-   "    --mcsat-nra-nlsat         Use NLSAT projection instead of Brown's single-cell construction\n"
-   "    --mcsat-nra-bound         Search by increasing the bound on variable magnitude\n"
-   "    --mcsat-nra-bound-min=<B> Set initial lower bound\n"
-   "    --mcsat-nra-bound-max=<B> Set maximal bound for search"
-   ""
-#endif
-	 "\n"
-	 "For bug reports and other information, please see http://yices.csl.sri.com/\n");
-  fflush(stdout);
-}
-
-/*
- * Message for unrecognized options or other errors on the command line.
- */
-static void print_usage(const char *progname) {
-  fprintf(stderr, "Usage: %s [options] filename\n", progname);
-  fprintf(stderr, "Try '%s --help' for more information\n", progname);
-}
-
-
-/*
- * Parse the command line and process options
- */
-static void parse_command_line(int argc, char *argv[]) {
-  cmdline_parser_t parser;
-  cmdline_elem_t elem;
-  optid_t k;
-  int32_t v;
-  int code;
-
-  filename = NULL;
-  incremental = false;
-  interactive = false;
-  show_stats = false;
-  verbosity = 0;
-  timeout = 0;
-  nthreads = 0;
-
-  mcsat = false;
-  mcsat_nra_mgcd = false;
-  mcsat_nra_nlsat = false;
-  mcsat_nra_bound = false;
-  mcsat_nra_bound_min = -1;
-  mcsat_nra_bound_max = -1;
-
-  init_pvector(&trace_tags, 5);
-
-  init_cmdline_parser(&parser, options, NUM_OPTIONS, argv, argc);
-
-  for (;;) {
-    cmdline_parse_element(&parser, &elem);
-    switch (elem.status) {
-    case cmdline_done:
-      goto done;
-
-    case cmdline_argument:
-      if (filename == NULL) {
-	filename = elem.arg;
-      } else {
-	fprintf(stderr, "%s: too many arguments\n", parser.command_name);
-	print_usage(parser.command_name);
-	code = YICES_EXIT_USAGE;
-	goto exit;
-      }
-      break;
-
-    case cmdline_option:
-      k = elem.key;
-      switch (k) {
-      case show_version_opt:
-	print_version();
-	code = YICES_EXIT_SUCCESS;
-	goto exit;
-
-      case show_help_opt:
-	print_help(parser.command_name);
-	code = YICES_EXIT_SUCCESS;
-	goto exit;
-
-      case show_stats_opt:
-	show_stats = true;
-	break;
-
-      case verbosity_opt:
-	v = elem.i_value;
-	if (v < 0) {
-	  fprintf(stderr, "%s: the verbosity level must be non-negative\n", parser.command_name);
-	  print_usage(parser.command_name);
-	  code = YICES_EXIT_USAGE;
-	  goto exit;
-	}
-	verbosity = v;
-	break;
-
-      case timeout_opt:
-	v = elem.i_value;
-	if (v < 0) {
-	  fprintf(stderr, "%s: the timeout must be non-negative\n", parser.command_name);
-	  print_usage(parser.command_name);
-	  code = YICES_EXIT_USAGE;
-	  goto exit;
-	}
-	timeout = v;
-	break;
-
-      case nthreads_opt:
-	v = elem.i_value;
-	if (v < 0) {
-	  fprintf(stderr, "%s: the number of threads must be non-negative\n", parser.command_name);
-	  print_usage(parser.command_name);
-	  code = YICES_EXIT_USAGE;
-	  goto exit;
-	}
-	nthreads = v;
-	break;
-	
-      case incremental_opt:
-	incremental = true;
-	break;
-
-      case interactive_opt:
-	interactive = true;
-	break;
-
-      case mcsat_opt:
-#if HAVE_MCSAT
-        mcsat = true;
-#else
-	fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name);
-	code = YICES_EXIT_USAGE;
-	goto exit;
-#endif
-        break;
-
-      case mcsat_nra_mgcd_opt:
-#if HAVE_MCSAT
-        mcsat_nra_mgcd = true;
-#else
-        fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name);
-        code = YICES_EXIT_USAGE;
-        goto exit;
-#endif
-        break;
-
-      case mcsat_nra_nlsat_opt:
-#if HAVE_MCSAT
-        mcsat_nra_nlsat = true;
-#else
-        fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name);
-        code = YICES_EXIT_USAGE;
-        goto exit;
-#endif
-        break;
-
-      case mcsat_nra_bound_opt:
-#if HAVE_MCSAT
-        mcsat_nra_bound = true;
-#else
-        fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name);
-        code = YICES_EXIT_USAGE;
-        goto exit;
-#endif
-        break;
-
-      case mcsat_nra_bound_min_opt:
-#if HAVE_MCSAT
-        v = elem.i_value;
-        if (v < 0) {
-          fprintf(stderr, "%s: the min value must be non-negative\n", parser.command_name);
-          print_usage(parser.command_name);
-          code = YICES_EXIT_USAGE;
-          goto exit;
-        }
-        mcsat_nra_bound_min = v;
-#else
-        fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name);
-        code = YICES_EXIT_USAGE;
-        goto exit;
-#endif
-        break;
-
-      case mcsat_nra_bound_max_opt:
-#if HAVE_MCSAT
-        v = elem.i_value;
-        if (v < 0) {
-          fprintf(stderr, "%s: the max value must be non-negative\n", parser.command_name);
-          print_usage(parser.command_name);
-          code = YICES_EXIT_USAGE;
-          goto exit;
-        }
-        mcsat_nra_bound_max = v;
-#else
-        fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name);
-        code = YICES_EXIT_USAGE;
-        goto exit;
-#endif
-        break;
-
-      case trace_opt:
-        pvector_push(&trace_tags, elem.s_value);
-        break;
-      }
-      break;
-
-    case cmdline_error:
-      cmdline_print_error(&parser, &elem);
-      fprintf(stderr, "Try %s --help for more information\n", parser.command_name);
-      code = YICES_EXIT_USAGE;
-      goto exit;
-    }
-  }
-
- done:
-
-  // force interactive to false if there's a filename
-  if (filename != NULL) {
-    interactive = false;
-  }
-  return;
-
- exit:
-  // cleanup then exit
-  // code is either YICES_EXIT_SUCCESS or YICES_EXIT_USAGE.
-  delete_pvector(&trace_tags);
-  exit(code);
-}
-
-static void setup_mcsat(void) {
-  aval_t aval_true;
-
-  if (mcsat) {
-    smt2_enable_mcsat();
-  }
-
-  aval_true = attr_vtbl_symbol(__smt2_globals.avtbl, "true");
-
-  if (mcsat_nra_mgcd) {
-    smt2_set_option(":yices-mcsat-nra-mgcd", aval_true);
-  }
-
-  if (mcsat_nra_nlsat) {
-    smt2_set_option(":yices-mcsat-nra-nlsat", aval_true);
-  }
-
-  if (mcsat_nra_bound) {
-    smt2_set_option(":yices-mcsat-nra-bound", aval_true);
-  }
-
-  if (mcsat_nra_bound_min >= 0) {
-    aval_t aval_bound_min;
-    rational_t q;
-    q_init(&q);
-    q_set32(&q, mcsat_nra_bound_min);
-    aval_bound_min = attr_vtbl_rational(__smt2_globals.avtbl, &q);
-    smt2_set_option(":yices-mcsat-nra-bound-min", aval_bound_min);
-    q_clear(&q);
-  }
-
-  if (mcsat_nra_bound_max >= 0) {
-    aval_t aval_bound_max;
-    rational_t q;
-    q_init(&q);
-    q_set32(&q, mcsat_nra_bound_max);
-    aval_bound_max = attr_vtbl_rational(__smt2_globals.avtbl, &q);
-    smt2_set_option(":yices-mcsat-nra-bound-max", aval_bound_max);
-    q_clear(&q);
-  }
-}
-
-
-/********************
- *  SIGNAL HANDLER  *
- *******************/
-
-static const char signum_msg[24] = "\nInterrupted by signal ";
-static char signum_buffer[100];
-
-/*
- * Write signal number of file 2 (assumed to be stderr): we can't use
- * fprintf because it's not safe in a signal handler.
- */
-static void write_signum(int signum) {
-  ssize_t w;
-  uint32_t i, n;
-
-  memcpy(signum_buffer, signum_msg, sizeof(signum_msg));
-
-  // force signum to be at most two digits
-  signum = signum % 100;
-  n = sizeof(signum_msg);
-  if (signum > 10) {
-    signum_buffer[n] = (char)('0' + signum/10);
-    signum_buffer[n + 1] = (char)('0' + signum % 10);
-    signum_buffer[n + 2] = '\n';
-    n += 3;
-  } else {
-    signum_buffer[n] = (char)('0' + signum);
-    signum_buffer[n + 1] = '\n';
-    n += 2;
-  }
-
-  // write to file 2
-  i = 0;
-  do {
-    do {
-      w = write(2, signum_buffer + i, n);
-    } while (w < 0 && errno == EAGAIN);
-    if (w < 0) break; // write error, we can't do much about it.
-    i += (uint32_t) w;
-    n -= (uint32_t) w;
-  } while (n > 0);
-}
-
-/*
- * We call exit on SIGINT/ABORT and XCPU
- * - we could try to handle SIGINT more gracefully in interactive mode
- * - this will do for now.
- */
-static void default_handler(int signum) {
-  if (verbosity > 0) {
-    write_signum(signum);
-  }
-  if (show_stats) {
-    smt2_show_stats();
-  }
-  _exit(YICES_EXIT_INTERRUPTED);
-}
-
-
-/*
- * Initialize the signal handlers
- */
-static void init_handlers(void) {
-  signal(SIGINT, default_handler);
-  signal(SIGABRT, default_handler);
-#ifndef MINGW
-  signal(SIGXCPU, default_handler);
-#endif
-}
-
-
-/*
- * Reset the default handlers
- */
-static void reset_handlers(void) {
-  signal(SIGINT, SIG_DFL);
-  signal(SIGABRT, SIG_DFL);
-#ifndef MINGW
-  signal(SIGXCPU, SIG_DFL);
-#endif
-}
-
-
-
-/**********
- *  MAIN  *
- *********/
-
-#define HACK_FOR_UTF 0
-
-#if HACK_FOR_UTF
-
-/*
- * List of locales to try
- */
-#define NUM_LOCALES 3
-
-static const char *const locales[NUM_LOCALES] = {
-  "C.UTF-8", "en_US.utf8", "en_US.UTF-8",
-};
-
-// HACK TO FORCE UTF8
-static void force_utf8(void) {
-  uint32_t i;
-
-  for (i=0; i<NUM_LOCALES; i++) {
-    if (setlocale(LC_CTYPE, locales[i]) != NULL) {
-      if (verbosity > 1) {
-	fprintf(stderr, "Switched to locale '%s'\n", setlocale(LC_CTYPE, NULL));
-	fflush(stderr);
-      }
-      return;
-    }
-  }
-
-  fprintf(stderr, "Failed to switch locale to UTF-8. Current locale is '%s'\n", setlocale(LC_CTYPE, NULL));
-  fflush(stderr);
-}
-
-#else
-
-static void force_utf8(void) {
-  // Do nothing
-}
-
-#endif
-
-int main(int argc, char *argv[]) {
-  int32_t code;
-  uint32_t i;
-
-  parse_command_line(argc, argv);
-  force_utf8();
-
-  if (filename != NULL) {
-    // read from file
-    if (init_smt2_file_lexer(&lexer, filename) < 0) {
-      perror(filename);
-      exit(YICES_EXIT_FILE_NOT_FOUND);
-    }
-  } else {
-    // read from stdin
-    init_smt2_stdin_lexer(&lexer);
-  }
-
-  init_handlers();
-
-  yices_init();
-  init_mt2(!incremental, timeout, nthreads, interactive);
-  init_smt2_tstack(&stack);
-  init_parser(&parser, &lexer, &stack);
-
-  init_parameter_name_table();
-  
-  if (verbosity > 0) {
-    smt2_set_verbosity(verbosity);
-  }
-  if (trace_tags.size > 0) {
-    for (i = 0; i < trace_tags.size; ++ i) {
-      smt2_enable_trace_tag(trace_tags.data[i]);
-    }
-  }
-
-  setup_mcsat();
-
-  while (smt2_active()) {
-    if (interactive) {
-      // prompt
-      fputs("yices> ", stderr);
-      fflush(stderr);
-    }
-    code = parse_smt2_command(&parser);
-    if (code < 0) {
-      // syntax error
-      if (interactive) {
-	flush_lexer(&lexer);
-      } else {
-	break; // exit
-      }
-    }
-  }
-
-  if (show_stats) {
-    smt2_show_stats();
-  }
-
-  delete_pvector(&trace_tags);
-  delete_parser(&parser);
-  close_lexer(&lexer);
-  delete_tstack(&stack);
-  delete_smt2();
-  yices_exit();
-
-  reset_handlers();
-
-  return YICES_EXIT_SUCCESS;
-}
-
diff --git a/src/frontend/yices_smtcomp.c b/src/frontend/yices_smtcomp.c
index 89c53cee9..f6a4f41ad 100644
--- a/src/frontend/yices_smtcomp.c
+++ b/src/frontend/yices_smtcomp.c
@@ -184,6 +184,8 @@ static tracer_t tracer;
  */
 static uint32_t timeout;
 
+static timeout_t *to;
+
 /*
  * Input file given on the command line.
  * If this is NULL, we read from stdin.
@@ -1292,14 +1294,14 @@ static int process_benchmark(void) {
     start_search_time = get_cpu_time();
 
     if (timeout > 0) {
-      init_timeout();
-      start_timeout(timeout, timeout_handler, &context);
+      to = init_timeout();
+      start_timeout(to, timeout, timeout_handler, &context);
     }
     code = check_context(&context, &params);
     clear_handler();
     if (timeout > 0) {
-      clear_timeout();
-      delete_timeout();
+      clear_timeout(to);
+      delete_timeout(to);
     }
     print_results();
 
diff --git a/src/mcsat/bv/bv_explainer.c b/src/mcsat/bv/bv_explainer.c
index 6de49c802..9521bb600 100644
--- a/src/mcsat/bv/bv_explainer.c
+++ b/src/mcsat/bv/bv_explainer.c
@@ -178,7 +178,7 @@ void bv_explainer_check_conflict(bv_explainer_t* exp, const ivector_t* conflict)
   smt_status_t result = yices_check_context(ctx, NULL);
   (void) result;
   assert(result == STATUS_UNSAT);
-  yices_free_context(ctx);
+  _o_yices_free_context(ctx);
 }
 
 void print_counters(bv_explainer_t* exp){
diff --git a/src/mcsat/bv/explain/arith_norm.c b/src/mcsat/bv/explain/arith_norm.c
index 65b8a4a0e..d78d31f10 100644
--- a/src/mcsat/bv/explain/arith_norm.c
+++ b/src/mcsat/bv/explain/arith_norm.c
@@ -777,7 +777,9 @@ term_t arith_normalise_upto(arith_norm_t* norm, term_t u, uint32_t w){
 
   case BV_ARRAY: {  // Concatenated boolean terms
     composite_term_t* concat_desc = bvarray_term_desc(terms, t);
-    term_t ebits[w]; // Where we build the result
+    term_t *ebits; // Where we build the result
+
+    ebits = (term_t *) safe_malloc(w * sizeof(term_t));
 
     // First, we eliminate BIT_TERM-over-BV_ARRAYs:
     for (uint32_t i = 0; i < w; i++)
@@ -791,7 +793,11 @@ term_t arith_normalise_upto(arith_norm_t* norm, term_t u, uint32_t w){
     // preproc[1][i] is the term_t arith_normalise_upto(k,top+1) (normalised version of k over the lowest top+1 bits), let's call it norm
     // preproc[2][i] is the value returned by bv_evaluator_not_free_up_to(norm), let's call it maxeval
     // preproc[3][i] is the term_t arith_normalise_upto(norm,maxeval), if maxeval is not 0
-    term_t preproc[4][w];
+
+    term_t *preproc[4];
+    for (int i = 0; i < 4; i ++)
+      preproc[i] = (term_t *) safe_malloc(4 * w * sizeof(term_t));
+    
     // We initialise the hashmap
     fix_htbl_init(preproc[0], w);
       
@@ -865,6 +871,11 @@ term_t arith_normalise_upto(arith_norm_t* norm, term_t u, uint32_t w){
     arith_analyse_t analysis;
     init_analysis(&analysis);
     analyse_bvarray(norm, w, ebits, &analysis);
+
+    for (int i = 0; i < 4; i ++)
+      safe_free(preproc[i]);
+    safe_free(ebits);
+    
     return finalise(norm, t, &analysis);
   }
 
diff --git a/src/mt/threads.h b/src/mt/threads.h
index 9e293e5a9..9f4a40f12 100644
--- a/src/mt/threads.h
+++ b/src/mt/threads.h
@@ -22,6 +22,8 @@
 #include <stdint.h>
 #include <stdbool.h>
 
+#include "utils/error.h"
+
 /* the thread main */
 #ifdef MINGW
 #define YICES_THREAD_ATTR  __stdcall
@@ -58,5 +60,17 @@ extern void mt_test_usage(int32_t argc, char* argv[]);
 
 extern yices_thread_result_t yices_thread_exit(void);
 
+/*
+ * Wrap around a thread API call. If the API call indicates error,
+ * print the message, a description of the error, and exit.
+ */
+#ifndef MINGW
+#define check_thread_api(expr, msg) (expr)
+#else
+static inline void check_thread_api(int expr, const char *msg) {
+  if (expr)
+    perror_fatal_code(msg, expr);
+}
+#endif
 
 #endif /* __THREADS_H */
diff --git a/src/mt/threads_posix.c b/src/mt/threads_posix.c
index 61d051010..14d043aa4 100644
--- a/src/mt/threads_posix.c
+++ b/src/mt/threads_posix.c
@@ -21,14 +21,21 @@
 #include <errno.h>
 #include <string.h>
 #include <pthread.h>
+#include <sys/resource.h>
+
+#include "utils/error.h"
 
 void launch_threads(int32_t nthreads, void* extras, size_t extra_sz, const char* test, yices_thread_main_t thread_main, bool verbose){
-  int32_t retcode, thread;
+  int32_t thread;
   char  buff[1024];
 
   thread_data_t* tdata = (thread_data_t*)calloc(nthreads, sizeof(thread_data_t)); 
 
   pthread_t* tids = (pthread_t*)calloc(nthreads, sizeof(pthread_t));
+  pthread_attr_t attr;
+  size_t stacksize;
+  struct rlimit rlp;
+  
   if((tdata == NULL) || (tids == NULL)){
     fprintf(stderr, "Couldn't alloc memory for %d threads\n", nthreads);
     exit(EXIT_FAILURE);
@@ -38,6 +45,16 @@ void launch_threads(int32_t nthreads, void* extras, size_t extra_sz, const char*
     printf("%d threads\n", nthreads);
   }
 
+  /* Give child threads the same stack size as the main thread. */
+  if (getrlimit(RLIMIT_STACK, &rlp) == -1)
+    perror_fatal("launch_threads: getrlimit");
+  check_thread_api(pthread_attr_init(&attr),
+		   "launch_threads: pthread_attr_init");
+  check_thread_api(pthread_attr_getstacksize(&attr, &stacksize),
+		   "launch_threads: pthread_attr_getstacksize");
+  check_thread_api(pthread_attr_setstacksize(&attr, rlp.rlim_cur),
+		   "launch_threads: pthread_attr_setstacksize");
+    
   for(thread = 0; thread < nthreads; thread++){
     snprintf(buff, 1024, "/tmp/%s_%d.txt", test, thread);
     if(verbose){
@@ -48,29 +65,26 @@ void launch_threads(int32_t nthreads, void* extras, size_t extra_sz, const char*
       tdata[thread].extra = (extras + (thread * extra_sz));
     }
     tdata[thread].output = fopen(buff, "w");
-    if(tdata[thread].output == NULL){
-      fprintf(stderr, "fopen failed: %s\n", strerror(errno));
-      exit(EXIT_FAILURE);
-    }
+    if(tdata[thread].output == NULL)
+      perror_fatal("launch_threads: fopen");
 
-    retcode =  pthread_create(&tids[thread], NULL, thread_main, &tdata[thread]);
-    if(retcode){
-      fprintf(stderr, "pthread_create failed: %s\n", strerror(retcode));
-      exit(EXIT_FAILURE);
-    }
+    check_thread_api(pthread_create(&tids[thread], &attr, thread_main,
+				    &tdata[thread]),
+		     "launch_threads: pthread_create");
   }
 
+  check_thread_api(pthread_attr_destroy(&attr),
+		   "launch_threads: pthread_attr_destroy");
+    
+  
   if(verbose){
     printf("threads away\n\n");
   }
 
 
   for(thread = 0; thread < nthreads; thread++){
-    retcode = pthread_join(tids[thread], NULL);
-    if(retcode){
-      fprintf(stderr, "pthread_join failed: %s\n", strerror(retcode));
-      exit(EXIT_FAILURE);
-    }
+    check_thread_api(pthread_join(tids[thread], NULL),
+		     "launch_threads: pthread_join");
     fclose(tdata[thread].output);
   }
 
diff --git a/src/mt/yices_locks_posix.c b/src/mt/yices_locks_posix.c
index 827e7f584..821b809df 100644
--- a/src/mt/yices_locks_posix.c
+++ b/src/mt/yices_locks_posix.c
@@ -23,6 +23,7 @@
 #include <string.h>
 
 #include "yices_locks.h"
+#include "threads.h"
 
 static void print_error(const char *caller, const char *syscall, int errnum) {
   char buffer[64];
@@ -33,27 +34,30 @@ static void print_error(const char *caller, const char *syscall, int errnum) {
 }
 
 int32_t create_yices_lock(yices_lock_t* lock){
-  int32_t retcode;
+  pthread_mutexattr_t *mattr = NULL;
+
 #ifndef NDEBUG
+  /* Make the mutex detect recursive locks. */
   pthread_mutexattr_t mta;
-  pthread_mutexattr_t *mattr = &mta;
-#else
-  pthread_mutexattr_t *mattr = NULL;
+
+  mattr = &mta;
+
+  check_thread_api(pthread_mutexattr_init(mattr),
+		   "create_yices_lock: pthread_mutexattr_init");
+  check_thread_api(pthread_mutexattr_settype(mattr,
+					     PTHREAD_MUTEX_ERRORCHECK),
+		   "create_yices_lock: pthread_mutextattr_settype");
 #endif
 
+  check_thread_api(pthread_mutex_init(lock, mattr),
+		   "create_yices_lock: pthread_mutex_init");
+
 #ifndef NDEBUG
-  retcode = pthread_mutexattr_init(mattr);
-  if(retcode)
-    print_error("create_yices_lock", "pthread_mutexattr_init", retcode);
-  retcode = pthread_mutexattr_settype(mattr, PTHREAD_MUTEX_ERRORCHECK);
-  if(retcode)
-    print_error("create_yices_lock", "pthread_mutextattr_settype", retcode);
+  check_thread_api(pthread_mutexattr_destroy(mattr),
+		   "create_yices_lock: pthread_mutexattr_destroy");
 #endif
-  retcode = pthread_mutex_init(lock, mattr);
-  if(retcode)
-    print_error("create_yices_lock", "pthread_mutex_init", retcode);
-  assert(retcode == 0);
-  return retcode;
+
+  return 0;
 }
 
 int32_t try_yices_lock(yices_lock_t* lock){
@@ -71,27 +75,20 @@ int32_t try_yices_lock(yices_lock_t* lock){
 
 
 int32_t get_yices_lock(yices_lock_t* lock){
-  int32_t retcode = pthread_mutex_lock(lock);
-  if(retcode){
-    print_error("get_yices_lock", "pthread_mutex_lock", retcode);
-  }
-  assert(retcode == 0);
-  return retcode;
+  check_thread_api(pthread_mutex_lock(lock),
+		   "get_yices_lock: pthread_mutex_lock");
+
+  return 0;
 }
 
 int32_t release_yices_lock(yices_lock_t* lock){
-  int32_t retcode = pthread_mutex_unlock(lock);
-  if(retcode){
-    print_error("release_yices_lock", "pthread_mutex_unlock", retcode);
-  }
-  assert(retcode == 0);
-  return retcode;
+  check_thread_api(pthread_mutex_unlock(lock),
+		   "release_yices_lock: pthread_mutex_unlock");
+
+  return 0;
 }
 
 void destroy_yices_lock(yices_lock_t* lock){
-  int32_t retcode = pthread_mutex_destroy(lock);
-  if(retcode){
-    print_error("destroy_yices_lock", "pthread_mutex_destroy", retcode);
-  }
-  assert(retcode == 0);
+  check_thread_api(pthread_mutex_destroy(lock),
+		   "destroy_yices_lock: pthread_mutex_destroy");
 }
diff --git a/src/utils/error.c b/src/utils/error.c
new file mode 100644
index 000000000..fee3577e1
--- /dev/null
+++ b/src/utils/error.c
@@ -0,0 +1,36 @@
+/*
+ * This file is part of the Yices SMT Solver.
+ * Copyright (C) 2023 SRI International.
+ *
+ * Yices is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * Yices is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+#include "yices_exit_codes.h"
+
+void perror_fatal(const char *s) {
+  perror(s);
+  exit(YICES_EXIT_INTERNAL_ERROR);
+}
+
+void perror_fatal_code(const char *s, int err) {
+  char buffer[64];
+  
+  strerror_r(err, buffer, sizeof(buffer));
+  fprintf(stderr, "%s: %s\n", s, buffer);
+  exit(YICES_EXIT_INTERNAL_ERROR);
+}
diff --git a/src/utils/error.h b/src/utils/error.h
new file mode 100644
index 000000000..02d29d556
--- /dev/null
+++ b/src/utils/error.h
@@ -0,0 +1,29 @@
+/*
+ * This file is part of the Yices SMT Solver.
+ * Copyright (C) 2023 SRI International.
+ *
+ * Yices is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * Yices is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef __ERROR_H
+#define __ERROR_H
+
+/* Like perror, but exit after printing the message. */
+extern void perror_fatal(const char *s);
+			 
+/* Like perror, but use ERR as the error code and exit after printing
+   the message. */
+extern void perror_fatal_code(const char *s, int err);
+
+#endif
diff --git a/src/utils/timeout.c b/src/utils/timeout.c
index 3dadd02b4..80518f5bd 100644
--- a/src/utils/timeout.c
+++ b/src/utils/timeout.c
@@ -43,16 +43,55 @@
  */
 
 #include <assert.h>
+#if !defined(MINGW) && defined(THREAD_SAFE)
+#include <pthread.h>
+#include <sys/time.h>
+#endif
 
+#include "utils/error.h"
+#include "utils/memalloc.h"
 #include "utils/timeout.h"
 #include "yices_exit_codes.h"
 
+/*
+ * Timeout state:
+ * - NOT_READY: initial state and after call to delete_timeout
+ * - READY: ready to be started (state after init_timeout
+ *          and after clear_timeout)
+ * - ACTIVE: after a call to start_timeout, before the timer fires
+ *           or the timeout is canceled
+ * - CANCELED: used by clear_timeout
+ * - FIRED: after the handler has been called
+ */
+typedef enum timeout_state {
+  TIMEOUT_NOT_READY, // 0
+  TIMEOUT_READY,
+  TIMEOUT_ACTIVE,
+  TIMEOUT_CANCELED,
+  TIMEOUT_FIRED,
+} timeout_state_t;
+
+
+typedef struct timeout_s {
+  timeout_state_t state;
+  timeout_handler_t handler;
+  void *param;
+#ifdef THREAD_SAFE
+  struct timespec ts;
+  pthread_t thread;
+  pthread_mutex_t mutex;
+  pthread_cond_t cond;
+#endif
+} timeout_t;
+
+#ifndef THREAD_SAFE
 
 /*
  * Global structure common to both implementation.
  */
 static timeout_t the_timeout;
 
+#endif
 
 #ifndef MINGW
 
@@ -65,7 +104,110 @@ static timeout_t the_timeout;
 #include <signal.h>
 #include <stdio.h>
 #include <stdlib.h>
+#include <sys/errno.h>
+
+#ifdef THREAD_SAFE
+
+#include "mt/threads.h"
 
+timeout_t *init_timeout(void) {
+  timeout_t *timeout;
+
+  timeout = (timeout_t *) safe_malloc(sizeof(timeout_t));
+
+  timeout->state = TIMEOUT_READY;
+  timeout->handler = NULL;
+  timeout->param = NULL;
+  timeout->ts.tv_sec = 0;
+  timeout->ts.tv_nsec = 0;
+
+  check_thread_api(pthread_mutex_init(&timeout->mutex, /*attr=*/NULL),
+		   "start_timeout: pthread_mutex_init");
+  check_thread_api(pthread_cond_init(&timeout->cond, /*attr=*/NULL),
+		   "start_timeout: pthread_cond_init");
+  
+  return timeout;
+}
+
+void delete_timeout(timeout_t *timeout) {
+  check_thread_api(pthread_cond_destroy(&timeout->cond),
+		   "delete_timeout: pthread_cond_destroy");
+  check_thread_api(pthread_mutex_destroy(&timeout->mutex),
+		   "delete_timeout: pthread_mutex_destroy");
+    
+  safe_free(timeout);
+}
+
+static void *timer_thread(void *arg) {
+  timeout_t *timeout;
+  
+  timeout = (timeout_t *) arg;
+
+  /* Get exclusive access to the state. */
+  check_thread_api(pthread_mutex_lock(&timeout->mutex),
+		   "timer_thread: pthread_mutex_lock");
+  /* It is theoretically possible that the timeout has already been
+     canceled by a quick call to clear_timeout. If so, we do not need
+     to wait. */
+  if (timeout->state != TIMEOUT_CANCELED) {
+    int ret = pthread_cond_timedwait(&timeout->cond, &timeout->mutex,
+				     &timeout->ts);
+    if (ret && ret != ETIMEDOUT)
+      perror_fatal_code("timer_thread: pthread_cond_timedwait", ret);
+  }
+
+  /* If the timeout wasn't canceled, then the timeout expired. */
+  if (timeout->state != TIMEOUT_CANCELED) {
+    timeout->state = TIMEOUT_FIRED;
+    timeout->handler(timeout->param);
+  }
+
+  check_thread_api(pthread_mutex_unlock(&timeout->mutex),
+		   "timer_thread: pthread_mutex_unlock");
+  
+  return NULL;
+}
+
+void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param) {
+  struct timeval tv;
+  
+  assert(delay > 0 && timeout->state == TIMEOUT_READY && handler != NULL);
+
+  timeout->state = TIMEOUT_ACTIVE;
+  timeout->handler = handler;
+  timeout->param = param;
+
+  /* Compute the desired stop time. */
+  if (gettimeofday(&tv, /*tzp=*/NULL) == -1)
+    perror_fatal("start_timeout: gettimeofday");
+  timeout->ts.tv_sec = tv.tv_sec + delay;
+  timeout->ts.tv_nsec = 1000 * tv.tv_usec;
+
+  check_thread_api(pthread_create(&timeout->thread, /*attr=*/NULL,
+				  timer_thread, timeout),
+		   "start_timeout: pthread_create");
+}
+
+void clear_timeout(timeout_t *timeout) {
+  void *value;
+  
+  /* Tell the thread to exit. */
+  check_thread_api(pthread_mutex_lock(&timeout->mutex),
+		   "clear_timeout: pthread_mutex_lock");
+  timeout->state = TIMEOUT_CANCELED;
+  check_thread_api(pthread_mutex_unlock(&timeout->mutex),
+		   "clear_timeout: pthread_mutex_unlock");
+  check_thread_api(pthread_cond_signal(&timeout->cond),
+		   "clear_timeout: pthread_cond_signal");
+
+  /* Wait for the thread to exit. */
+  check_thread_api(pthread_join(timeout->thread, &value),
+		   "clear_timeout: pthread_join");
+
+  timeout->state = TIMEOUT_READY;
+}
+
+#else /* !defined(THREAD_SAFE) */
 
 /*
  * To save the original SIG_ALRM handler
@@ -92,7 +234,7 @@ static void alarm_handler(int signum) {
  * - install the alarm_handler (except on Solaris)
  * - initialize state to READY
  */
-void init_timeout(void) {
+timeout_t *init_timeout(void) {
 #ifndef SOLARIS
   saved_handler = signal(SIGALRM, alarm_handler);
   if (saved_handler == SIG_ERR) {
@@ -104,6 +246,8 @@ void init_timeout(void) {
   the_timeout.state = TIMEOUT_READY;;
   the_timeout.handler = NULL;
   the_timeout.param = NULL;
+
+  return &the_timeout;
 }
 
 
@@ -116,7 +260,8 @@ void init_timeout(void) {
  *
  * On Solaris: set the signal handler here.
  */
-void start_timeout(uint32_t delay, timeout_handler_t handler, void *param) {
+void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param) {
+  assert(timeout == &the_timeout);
   assert(delay > 0 && the_timeout.state == TIMEOUT_READY && handler != NULL);
   the_timeout.state = TIMEOUT_ACTIVE;
   the_timeout.handler = handler;
@@ -140,7 +285,9 @@ void start_timeout(uint32_t delay, timeout_handler_t handler, void *param) {
  * - cancel the timeout if it's not fired
  * - set state to READY
  */
-void clear_timeout(void) {
+void clear_timeout(timeout_t *timeout) {
+  assert(timeout == &the_timeout);
+  
   // TODO: Check whether we should block the signals here?
   if (the_timeout.state == TIMEOUT_ACTIVE) {
     // not fired;
@@ -156,7 +303,9 @@ void clear_timeout(void) {
  * - cancel the timeout if it's active
  * - restore the original handler
  */
-void delete_timeout(void) {
+void delete_timeout(timeout_t *timeout) {
+  assert(timeout == &the_timeout);
+  
   if (the_timeout.state == TIMEOUT_ACTIVE) {
     (void) alarm(0);
   }
@@ -164,6 +313,7 @@ void delete_timeout(void) {
   the_timeout.state = TIMEOUT_NOT_READY;
 }
 
+#endif /* defined(THREAD_SAFE) */
 
 #else
 
@@ -210,7 +360,7 @@ static VOID CALLBACK timer_callback(PVOID param, BOOLEAN timer_or_wait_fired) {
  * Initialization:
  * - create the timer queue
  */
-void init_timeout(void) {
+timeout_t *init_timeout(void) {
   timer_queue = CreateTimerQueue();
   if (timer_queue == NULL) {
     fprintf(stderr, "Yices: CreateTimerQueue failed with error code %"PRIu32"\n", (uint32_t) GetLastError());
@@ -221,6 +371,8 @@ void init_timeout(void) {
   the_timeout.state = TIMEOUT_READY;
   the_timeout.handler = NULL;
   the_timeout.param = NULL;
+
+  return &the_timeout;
 }
 
 
@@ -231,9 +383,10 @@ void init_timeout(void) {
  * - handler = handler to call if fired
  * - param = parameter for the handler
  */
-void start_timeout(uint32_t delay, timeout_handler_t handler, void *param) {
+void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param) {
   DWORD duetime;
 
+  assert(timeout == &the_timeout);
   assert(delay > 0 && the_timeout.state == TIMEOUT_READY && handler != NULL);
 
   duetime = delay * 1000; // delay in milliseconds
@@ -255,10 +408,12 @@ void start_timeout(uint32_t delay, timeout_handler_t handler, void *param) {
 /*
  * Delete the timer
  */
-void clear_timeout(void) {
+void clear_timeout(timeout_t *timeout) {
   // GetLastError returns DWORD, which is an unsigned 32bit integer
   uint32_t error_code;
 
+  assert(timeout == &the_timeout);
+
   if (the_timeout.state == TIMEOUT_ACTIVE || the_timeout.state == TIMEOUT_FIRED) {
     if (the_timeout.state == TIMEOUT_ACTIVE) {
       // active and not fired yet
@@ -292,7 +447,9 @@ void clear_timeout(void) {
  * Final cleanup:
  * - delete the timer_queue
  */
-void delete_timeout(void) {
+void delete_timeout(timeout_t *timeout) {
+  assert(timeout == &the_timeout);
+  
   if (! DeleteTimerQueueEx(timer_queue, INVALID_HANDLE_VALUE)) {
     fprintf(stderr, "Yices: DeleteTimerQueueEx failed with error code %"PRIu32"\n", (uint32_t) GetLastError());
     fflush(stderr);
diff --git a/src/utils/timeout.h b/src/utils/timeout.h
index 6fb3e78cb..009282d0e 100644
--- a/src/utils/timeout.h
+++ b/src/utils/timeout.h
@@ -53,26 +53,6 @@
 
 #include <stdint.h>
 
-
-/*
- * Timeout state:
- * - NOT_READY: initial state and after call to delete_timeout
- * - READY: ready to be started (state after init_timeout
- *          and after clear_timeout)
- * - ACTIVE: after a call to start_timeout, before the timer fires
- *           or the timeout is canceled
- * - CANCELED: used by clear_timeout
- * - FIRED: after the handler has been called
- */
-typedef enum timeout_state {
-  TIMEOUT_NOT_READY, // 0
-  TIMEOUT_READY,
-  TIMEOUT_ACTIVE,
-  TIMEOUT_CANCELED,
-  TIMEOUT_FIRED,
-} timeout_state_t;
-
-
 /*
  * Handler: a function with a single (void*) parameter
  * - should do something cheap and fast.
@@ -83,11 +63,7 @@ typedef void (*timeout_handler_t)(void *data);
 /*
  * Internal structure used to manage the timeout
  */
-typedef struct timeout_s {
-  timeout_state_t state;
-  timeout_handler_t handler;
-  void *param;
-} timeout_t;
+typedef struct timeout_s timeout_t;
 
 
 
@@ -98,7 +74,7 @@ typedef struct timeout_s {
 /*
  * Initialize internal structures
  */
-extern void init_timeout(void);
+extern timeout_t *init_timeout(void);
 
 
 /*
@@ -107,20 +83,20 @@ extern void init_timeout(void);
  * - handler = the handler to call
  * - param = data passed to the handler
  */
-extern void start_timeout(uint32_t delay, timeout_handler_t handler, void *param);
+extern void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param);
 
 
 /*
  * Cancel the timeout if it's not fired.
  * Cleanup any structure allocated by start timeout.
  */
-extern void clear_timeout(void);
+extern void clear_timeout(timeout_t *timeout);
 
 
 /*
  * Final cleanup
  */
-extern void delete_timeout(void);
+extern void delete_timeout(timeout_t *timeout);
 
 
 
diff --git a/tests/regress/check.sh b/tests/regress/check.sh
index 9cdc5013c..e2870e180 100755
--- a/tests/regress/check.sh
+++ b/tests/regress/check.sh
@@ -34,13 +34,33 @@
 # what's expected.
 #
 
-if test $# != 2 ; then
-   echo "Usage: $0 <test-directory> <bin-directory>"
+usage() {
+   echo "Usage: $0 <test-directory> <bin-directory> [test1] [test2] ..."
    exit
+}
+    
+smt2_options=
+
+while getopts "s:" o; do
+    case "$o" in
+	s)
+	    smt2_options=${OPTARG}
+	    ;;
+	*)
+	    usage
+	    ;;
+    esac
+done
+shift $((OPTIND-1))
+
+if test $# "<" 2 ; then
+    usage
 fi
 
 regress_dir=$1
 bin_dir=$2
+shift 2
+all_tests="$@"
 
 # Make sure fatal errors go to stderr
 export LIBC_FATAL_STDERR_=1
@@ -112,11 +132,13 @@ else
     MCSAT_FILTER="."
 fi
 
-all_tests=$(
-    find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' |
-    grep $REGRESS_FILTER | grep $MCSAT_FILTER |
-    sort
-)
+if test -z "$all_tests"; then
+    all_tests=$(
+	find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' |
+	    grep $REGRESS_FILTER | grep $MCSAT_FILTER |
+	    sort
+    )
+fi
 
 for file in $all_tests; do
 
@@ -125,9 +147,12 @@ for file in $all_tests; do
     # Get the binary based on the filename
     filename=`basename "$file"`
 
+    options=
+    
     case $filename in
         *.smt2)
             binary=yices_smt2
+	    options=$smt2_options
             ;;
         *.smt)
             binary=yices_smtcomp
@@ -144,11 +169,10 @@ for file in $all_tests; do
     # Get the options
     if [ -e "$file.options" ]
     then
-        options=`cat $file.options`
+        options="$options `cat $file.options`"
         echo " [ $options ]"
     	test_string="$file [ $options ]"
     else
-        options=
         test_string="$file"
         echo
     fi
@@ -172,12 +196,13 @@ for file in $all_tests; do
       ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null
       (time ./$bin_dir/$binary $options ./$file >& $outfile ) >& $timefile
     )
+    status=$?
     thetime=`cat $timefile`
 
     # Do the diff
     DIFF=`diff -w $outfile $gold`
 
-    if [ $? -eq 0 ]
+    if [ $? -eq 0 ] && [ $status -eq 0 ]
     then
         echo -n $green
     	echo PASS [${thetime} s]
diff --git a/tests/unit/test_timeout.c b/tests/unit/test_timeout.c
index 0af1a1606..e780ae640 100644
--- a/tests/unit/test_timeout.c
+++ b/tests/unit/test_timeout.c
@@ -92,16 +92,16 @@ static void show_counter(uint32_t *c, uint32_t n) {
 /*
  * Test: n = size of the counter, t = timeout value
  */
-static void test_timeout(uint32_t *c, uint32_t n, uint32_t timeout) {
+static void test_timeout(timeout_t *to, uint32_t *c, uint32_t n, uint32_t timeout) {
   double start, end;
 
   printf("---> test: size = %"PRIu32", timeout = %"PRIu32" s\n", n, timeout);
   fflush(stdout);
   wrapper.interrupted  = false;
-  start_timeout(timeout, handler, &wrapper);
+  start_timeout(to, timeout, handler, &wrapper);
   start = get_cpu_time();
   loop(c, n);
-  clear_timeout();
+  clear_timeout(to);
   end = get_cpu_time();
   printf("     cpu time = %.2f s\n", end - start);
   fflush(stdout);
@@ -127,15 +127,16 @@ static uint32_t counter[64];
 int main(void) {
   uint32_t n;
   uint32_t time;
-
-  init_timeout();
+  timeout_t *timeout;
+  
+  timeout = init_timeout();
 
   time = 20;
   for (n=5; n<40; n++) {
-    test_timeout(counter, n, time);
+    test_timeout(timeout, counter, n, time);
   }
 
-  delete_timeout();
+  delete_timeout(timeout);
 
   return 0;
 }