diff --git a/src/exists_forall/ef_values.c b/src/exists_forall/ef_values.c
index 2bfc5f9bf..88368621f 100755
--- a/src/exists_forall/ef_values.c
+++ b/src/exists_forall/ef_values.c
@@ -557,7 +557,7 @@ void postprocess_ef_table(ef_table_t *vtable, bool check) {
       }
     }
   }
-  m = queue.size;
+  m = queue.capacity;
   j = 0;
   while(!int_queue_is_empty(&queue)) {
     tvalue = int_queue_pop(&queue);
diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c
index 801ca0e25..422c3a3f3 100644
--- a/src/mcsat/nra/nra_plugin.c
+++ b/src/mcsat/nra/nra_plugin.c
@@ -860,18 +860,24 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop,
         }
         lp_value_destruct(&v);
       }
-      // If the value is implied at zero level, propagate it
-      if (!nra->ctx->options->model_interpolation && !x_in_conflict && !trail_has_value(nra->ctx->trail, x) && trail_is_at_base_level(nra->ctx->trail)) {
-        const lp_feasibility_set_t* feasible = feasible_set_db_get(nra->feasible_set_db, x);
-        if (lp_feasibility_set_is_point(feasible)) {
+      if (!x_in_conflict && !trail_has_value(nra->ctx->trail, x)) {
+        const lp_feasibility_set_t *feasible_set = feasible_set_db_get(nra->feasible_set_db, x);
+        if (lp_feasibility_set_is_point(feasible_set)) {
           lp_value_t x_value;
           lp_value_construct_none(&x_value);
-          lp_feasibility_set_pick_value(feasible, &x_value);
+          lp_feasibility_set_pick_value(feasible_set, &x_value);
           if (lp_value_is_rational(&x_value)) {
-            mcsat_value_t value;
-            mcsat_value_construct_lp_value(&value, &x_value);
-            prop->add_at_level(prop, x, &value, nra->ctx->trail->decision_level_base);
-            mcsat_value_destruct(&value);
+            if (trail_is_at_base_level(nra->ctx->trail) && !nra->ctx->options->model_interpolation) {
+              mcsat_value_t value;
+              mcsat_value_construct_lp_value(&value, &x_value);
+              prop->add_at_level(prop, x, &value, nra->ctx->trail->decision_level_base);
+              mcsat_value_destruct(&value);
+            } else {
+              if (ctx_trace_enabled(nra->ctx, "nra::propagate")) {
+                ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", x);
+              }
+              nra->ctx->hint_next_decision(nra->ctx, x);
+            }
           }
           lp_value_destruct(&x_value);
         }
@@ -1069,7 +1075,7 @@ void nra_plugin_propagate(plugin_t* plugin, trail_token_t* prop) {
   }
 
   // Propagate
-  while(trail_is_consistent(trail) && nra->trail_i < trail_size(trail)) {
+  while (trail_is_consistent(trail) && nra->trail_i < trail_size(trail)) {
     // Current trail element
     var = trail_at(trail, nra->trail_i);
     nra->trail_i ++;
diff --git a/src/mcsat/plugin.h b/src/mcsat/plugin.h
index a75c506f9..685dbedce 100644
--- a/src/mcsat/plugin.h
+++ b/src/mcsat/plugin.h
@@ -113,6 +113,9 @@ struct plugin_context_s {
   /** Request a variable to be a top decision variable */
   void (*request_top_decision) (plugin_context_t* self, variable_t x);
 
+  /** Request a variable to be a next decision variable */
+  void (*hint_next_decision) (plugin_context_t* self, variable_t x);
+
 };
 
 /** Token to add entries to the trail */
@@ -334,10 +337,9 @@ void plugin_construct(plugin_t* plugin) {
   plugin->pop                       = NULL;
   plugin->build_model               = NULL;
   plugin->gc_mark                   = NULL;
-  plugin->gc_mark_and_clear          = NULL;
+  plugin->gc_mark_and_clear         = NULL;
   plugin->gc_sweep                  = NULL;
   plugin->set_exception_handler     = NULL;
 }
 
-
 #endif /* PLUGIN_H_ */
diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c
index 0a344fa84..05b175974 100644
--- a/src/mcsat/solver.c
+++ b/src/mcsat/solver.c
@@ -230,7 +230,10 @@ struct mcsat_solver_s {
   uint32_t plugins_count;
 
   /** Variable to decide on first */
-  variable_t top_decision_var;
+  ivector_t top_decision_vars;
+
+  /** Variables hinted by the plugins to decide next */
+  int_queue_t hinted_decision_vars;
 
   /** The queue for variable decisions */
   var_queue_t var_queue;
@@ -563,7 +566,7 @@ void trail_token_definition_lemma(trail_token_t* token, term_t lemma, term_t t)
   ivector_push(&tk->ctx->mcsat->plugin_definition_vars, t);
 }
 
-/** Concstruct the trail token */
+/** Construct the trail token */
 static inline
 void trail_token_construct(plugin_trail_token_t* token, mcsat_plugin_context_t* ctx, variable_t x) {
   token->token_interface.add = trail_token_add;
@@ -628,9 +631,18 @@ void mcsat_plugin_context_gc(plugin_context_t* self) {
 }
 
 static inline
-void mcsat_set_top_decision(mcsat_solver_t* mcsat, variable_t x) {
-  assert(mcsat->top_decision_var == variable_null);
-  mcsat->top_decision_var = x;
+void mcsat_add_top_decision(mcsat_solver_t* mcsat, variable_t x) {
+  for (int i = 0; i < mcsat->top_decision_vars.size; ++i) {
+    if (mcsat->top_decision_vars.data[i] == x) {
+      return;
+    }
+  }
+  ivector_push(&mcsat->top_decision_vars, x);
+}
+
+static inline
+void mcsat_add_decision_hint(mcsat_solver_t* mcsat, variable_t x) {
+  int_queue_push(&mcsat->hinted_decision_vars, x);
 }
 
 static inline
@@ -685,8 +697,15 @@ static
 void mcsat_plugin_context_request_top_decision(plugin_context_t* self, variable_t x) {
   mcsat_plugin_context_t* mctx;
   mctx = (mcsat_plugin_context_t*) self;
-  mcsat_set_top_decision(mctx->mcsat, x);
- }
+  mcsat_add_top_decision(mctx->mcsat, x);
+}
+
+static
+void mcsat_plugin_context_hint_next_decision(plugin_context_t* self, variable_t x) {
+  mcsat_plugin_context_t* mctx;
+  mctx = (mcsat_plugin_context_t*) self;
+  mcsat_add_decision_hint(mctx->mcsat, x);
+}
 
 static
 void mcsat_plugin_context_decision_calls(plugin_context_t* self, type_kind_t type) {
@@ -718,6 +737,7 @@ void mcsat_plugin_context_construct(mcsat_plugin_context_t* ctx, mcsat_solver_t*
   ctx->ctx.bump_variable_n = mcsat_plugin_context_bump_variable_n;
   ctx->ctx.cmp_variables = mcsat_plugin_context_cmp_variables;
   ctx->ctx.request_top_decision = mcsat_plugin_context_request_top_decision;
+  ctx->ctx.hint_next_decision = mcsat_plugin_context_hint_next_decision;
   ctx->mcsat = mcsat;
   ctx->plugin_name = plugin_name;
 }
@@ -860,7 +880,8 @@ void mcsat_construct(mcsat_solver_t* mcsat, const context_t* ctx) {
   preprocessor_construct(&mcsat->preprocessor, mcsat->terms, mcsat->exception, &mcsat->ctx->mcsat_options);
 
   // The variable queue
-  mcsat->top_decision_var = variable_null;
+  init_ivector(&mcsat->top_decision_vars, 0);
+  init_int_queue(&mcsat->hinted_decision_vars, 0);
   var_queue_construct(&mcsat->var_queue);
 
   mcsat->pending_requests_all.restart = false;
@@ -919,6 +940,8 @@ void mcsat_destruct(mcsat_solver_t* mcsat) {
   variable_db_destruct(mcsat->var_db);
   safe_free(mcsat->var_db);
   preprocessor_destruct(&mcsat->preprocessor);
+  delete_ivector(&mcsat->top_decision_vars);
+  delete_int_queue(&mcsat->hinted_decision_vars);
   var_queue_destruct(&mcsat->var_queue);
   delete_ivector(&mcsat->plugin_lemmas);
   delete_ivector(&mcsat->plugin_definition_lemmas);
@@ -994,6 +1017,9 @@ void mcsat_pop_internal(mcsat_solver_t* mcsat) {
     var_queue_insert(&mcsat->var_queue, unassigned->data[i]);
   }
   ivector_reset(unassigned);
+
+  // remove all the hints
+  int_queue_reset(&mcsat->hinted_decision_vars);
 }
 
 static
@@ -1159,7 +1185,7 @@ void mcsat_get_kind_owners(mcsat_solver_t* mcsat, term_t t, int_mset_t* owners)
 }
 
 
-static void mcsat_process_registeration_queue(mcsat_solver_t* mcsat) {
+static void mcsat_process_registration_queue(mcsat_solver_t* mcsat) {
   term_t t;
   uint32_t i, plugin_i;
   plugin_t* plugin;
@@ -1247,13 +1273,16 @@ void mcsat_gc(mcsat_solver_t* mcsat, bool mark_and_gc_internal) {
     gc_info_mark(&gc_vars, var);
     if (trace_enabled(mcsat->ctx->trace, "mcsat::gc")) {
       mcsat_trace_printf(mcsat->ctx->trace, "mcsat_gc(): marking ");
-       trace_term_ln(mcsat->ctx->trace, mcsat->terms, variable_db_get_term(mcsat->var_db, var));
+      trace_term_ln(mcsat->ctx->trace, mcsat->terms, variable_db_get_term(mcsat->var_db, var));
     }
   }
 
-  // Mark the top decision variable if any
-  if (mcsat->top_decision_var != variable_null) {
-    gc_info_mark(&gc_vars, mcsat->top_decision_var);
+  // Mark the decision hints if there are any
+  for (i = 0; i < int_queue_size(&mcsat->hinted_decision_vars); ++ i) {
+    gc_info_mark(&gc_vars, int_queue_at(&mcsat->hinted_decision_vars, i));
+  }
+  for (i = 0; i < mcsat->top_decision_vars.size; ++i) {
+    gc_info_mark(&gc_vars, mcsat->top_decision_vars.data[i]);
   }
 
   // Mark the trail variables as needed
@@ -1488,7 +1517,7 @@ void mcsat_assert_formula(mcsat_solver_t* mcsat, term_t f) {
   // Add the terms
   f_pos = unsigned_term(f);
   f_pos_var = variable_db_get_variable(mcsat->var_db, f_pos);
-  mcsat_process_registeration_queue(mcsat);
+  mcsat_process_registration_queue(mcsat);
 
   // Remember the assertion
   ivector_push(&mcsat->assertion_vars, f_pos_var);
@@ -1644,7 +1673,7 @@ void mcsat_add_lemma(mcsat_solver_t* mcsat, ivector_t* lemma, term_t decision_bo
     }
 
     // Process any newly registered variables
-    mcsat_process_registeration_queue(mcsat);
+    mcsat_process_registration_queue(mcsat);
 
     // Check if the literal has value (only negative allowed)
     if (trail_has_value(mcsat->trail, disjunct_pos_var)) {
@@ -2245,7 +2274,7 @@ bool mcsat_decide_assumption(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_ass
       break;
     }
 
-    // The variable (should exists already)
+    // The variable (should exist already)
     var_term = assumptions[mcsat->assumption_i];
     var = variable_db_get_variable_if_exists(mcsat->var_db, var_term);
     assert(var != variable_null);
@@ -2313,46 +2342,120 @@ bool mcsat_decide_assumption(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_ass
 }
 
 /**
- * Decides a variable using one of the plugins. Returns true if a variable
- * has been decided, or a conflict detected.
+ * Finds the correct plugin for var and asks it to make a decision.
+ * Returns true if a decision was made on var.
  */
 static
-bool mcsat_decide(mcsat_solver_t* mcsat) {
+bool mcsat_decide_var(mcsat_solver_t* mcsat, variable_t var, bool force_decision) {
+  // must be a valid variable that is not yet decided upon
+  assert(var != variable_null);
+  assert(!trail_has_value(mcsat->trail, var));
 
   uint32_t i;
-  variable_t var;
   plugin_t* plugin;
   plugin_trail_token_t decision_token;
+  bool made_decision = false;
+
+  // Get the owner that will decide that value of the variable
+  i = mcsat->decision_makers[variable_db_get_type_kind(mcsat->var_db, var)];
+  assert(i != MCSAT_MAX_PLUGINS);
+  // Construct the token
+  trail_token_construct(&decision_token, mcsat->plugins[i].plugin_ctx, var);
+  // Decide
+  if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) {
+    mcsat_trace_printf(mcsat->ctx->trace, "mcsat_decide(): with %s\n", mcsat->plugins[i].plugin_name);
+    mcsat_trace_printf(mcsat->ctx->trace, "mcsat_decide(): variable ");
+    variable_db_print_variable(mcsat->var_db, var, trace_out(mcsat->ctx->trace));
+    mcsat_trace_printf(mcsat->ctx->trace, "\n");
+  }
+  plugin = mcsat->plugins[i].plugin;
+
+  // Ask the owner to decide
+  mcsat_push_internal(mcsat);
+  assert(plugin->decide);
+  plugin->decide(plugin, var, (trail_token_t*) &decision_token, force_decision);
 
-  ivector_t skipped_variables; // Variables we took from the queue but plugin didn't decide
-  init_ivector(&skipped_variables, 0);
+  if (decision_token.used == 0) {
+    // If not decided, remember and go on
+    made_decision = false;
+    mcsat_pop_internal(mcsat);
+  } else {
+    made_decision = true;
+    // Decided, we can continue with the search
+    (*mcsat->solver_stats.decisions)++;
+    // Plugins are not allowed to cheat and decide on another variable
+    assert(trail_has_value(mcsat->trail, var));
+    if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) {
+      FILE* out = trace_out(mcsat->ctx->trace);
+      fprintf(out, "mcsat_decide(): value = ");
+      mcsat_value_print(trail_get_value(mcsat->trail, var), out);
+      fprintf(out, "\n");
+    }
+  }
+
+  // a forced decision implies a made decision
+  assert(!force_decision || made_decision);
+  return made_decision;
+}
+
+/**
+ * Decides a variable using one of the plugins. Returns true if a variable
+ * has been decided, or a conflict detected.
+ */
+static
+bool mcsat_decide(mcsat_solver_t* mcsat) {
 
   assert(!mcsat->trail->inconsistent);
 
+  ivector_t skipped_variables; // Variables we took from the queue but plugin didn't decide
+  init_ivector(&skipped_variables, 0);
+
+  variable_t var;
+  bool aux_choice; // indicates that var was not taken from the queue
   bool force_decision = false;
-  while (true) {
+  double rand_freq = mcsat->heuristic_params.random_decision_freq;
 
-    // Use the variable a plugin requested
-    var = mcsat->top_decision_var;
-    if (var != variable_null && trail_has_value(mcsat->trail, var)) {
+  while (true) {
+    var = variable_null;
+    aux_choice = true;
+
+    // Us the top variables first
+    for (uint32_t i = 0; i < mcsat->top_decision_vars.size; ++i) {
+      var = mcsat->top_decision_vars.data[i];
+      assert(var != variable_null);
+      if (!trail_has_value(mcsat->trail, var)) {
+        force_decision = true;
+        break;
+      }
       var = variable_null;
     }
 
+    // then try the variables a plugin requested
+    if (var == variable_null) {
+      while (!int_queue_is_empty(&mcsat->hinted_decision_vars)) {
+        var = int_queue_pop(&mcsat->hinted_decision_vars);
+        assert(var != variable_null);
+        if (!trail_has_value(mcsat->trail, var)) {
+          break;
+        }
+        var = variable_null;
+      }
+    }
+
     // If there is an order that was passed in, try that
     if (var == variable_null) {
       const ivector_t* order = &mcsat->ctx->mcsat_var_order;
       if (order->size > 0) {
-        uint32_t i;
         if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) {
           FILE* out = trace_out(mcsat->ctx->trace);
           fprintf(out, "mcsat_decide(): var_order is ");
-          for (i = 0; i < order->size; ++ i) {
+          for (uint32_t i = 0; i < order->size; ++ i) {
             term_print_to_file(out, mcsat->ctx->terms, order->data[i]);
             fprintf(out, " ");
           }
           fprintf(out, "\n");
         }
-        for (i = 0; var == variable_null && i < order->size; ++i) {
+        for (uint32_t i = 0; var == variable_null && i < order->size; ++i) {
           term_t ovar_term = order->data[i];
           variable_t ovar = variable_db_get_variable_if_exists(mcsat->var_db, ovar_term);
           if (ovar == variable_null) continue; // Some variables are not used
@@ -2364,20 +2467,22 @@ bool mcsat_decide(mcsat_solver_t* mcsat) {
       }
     }
 
-    // Random decision:
-    if (var == variable_null) {
+    // Random decision
+    if (var == variable_null && rand_freq > 0.0) {
       double* seed = &mcsat->heuristic_params.random_decision_seed;
-      double freq = mcsat->heuristic_params.random_decision_freq;
-      if (drand(seed) < freq && !var_queue_is_empty(&mcsat->var_queue)) {
+      if (drand(seed) < rand_freq && !var_queue_is_empty(&mcsat->var_queue)) {
         var = var_queue_random(&mcsat->var_queue, seed);
         if (trail_has_value(mcsat->trail, var)) {
           var = variable_null;
-        } else {
-          // fprintf(stderr, "random\n");
         }
       }
     }
 
+    if (var == variable_null) {
+      // No auxiliary choice performed
+      aux_choice = false;
+    }
+
     // Use the queue
     while (!var_queue_is_empty(&mcsat->var_queue) && var == variable_null) {
       // Get the next variable from the queue
@@ -2385,7 +2490,7 @@ bool mcsat_decide(mcsat_solver_t* mcsat) {
       // If already assigned go on
       if (trail_has_value(mcsat->trail, var)) {
         if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) {
-          FILE* out = trace_out(mcsat->ctx->trace);
+          FILE *out = trace_out(mcsat->ctx->trace);
           fprintf(out, "mcsat_decide(): skipping ");
           variable_db_print_variable(mcsat->var_db, var, out);
           fprintf(out, "\n");
@@ -2396,53 +2501,21 @@ bool mcsat_decide(mcsat_solver_t* mcsat) {
     }
 
     if (var != variable_null) {
-      // Get the owner that will decide that value of the variable
-      i = mcsat->decision_makers[variable_db_get_type_kind(mcsat->var_db, var)];
-      assert(i != MCSAT_MAX_PLUGINS);
-      // Construct the token
-      trail_token_construct(&decision_token, mcsat->plugins[i].plugin_ctx, var);
-      // Decide
-      if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) {
-        mcsat_trace_printf(mcsat->ctx->trace, "mcsat_decide(): with %s\n", mcsat->plugins[i].plugin_name);
-        mcsat_trace_printf(mcsat->ctx->trace, "mcsat_decide(): variable ");
-        variable_db_print_variable(mcsat->var_db, var, trace_out(mcsat->ctx->trace));
-        mcsat_trace_printf(mcsat->ctx->trace, "\n");
-      }
-      plugin = mcsat->plugins[i].plugin;
-
-      // Ask the owner to decide
-      mcsat_push_internal(mcsat);
-      assert(plugin->decide);
-      plugin->decide(plugin, var, (trail_token_t*) &decision_token, force_decision);
-
-      if (decision_token.used == 0) {
-        // If not decided, remember and go on
-        ivector_push(&skipped_variables, var);
-        mcsat_pop_internal(mcsat);
-      } else {
-        // Decided, we can continue with the search
-        (*mcsat->solver_stats.decisions)++;
-        // If plugin decided to cheat by deciding on another variable, put it back
-        if (!trail_has_value(mcsat->trail, var)) {
-          var_queue_insert(&mcsat->var_queue, var);
-        } else {
-          if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) {
-            FILE* out = trace_out(mcsat->ctx->trace);
-            fprintf(out, "mcsat_decide(): value = ");
-            mcsat_value_print(trail_get_value(mcsat->trail, var), out);
-            fprintf(out, "\n");
-          }
-        }
+      bool made_decision = mcsat_decide_var(mcsat, var, force_decision);
+      if (made_decision) {
         break;
+      } else if (!aux_choice) {
+        ivector_push(&skipped_variables, var);
       }
     } else {
+      assert(!aux_choice);
       // No variables left to decide
       if (skipped_variables.size == 0) {
         // Didn't skip any, we're done
         break;
       } else {
         // Put the skipped back in the queue, and continue but force next decision
-        for (i = 0; i < skipped_variables.size; ++ i) {
+        for (uint32_t i = 0; i < skipped_variables.size; ++ i) {
           var_queue_insert(&mcsat->var_queue, skipped_variables.data[i]);
         }
         ivector_reset(&skipped_variables);
@@ -2457,7 +2530,7 @@ bool mcsat_decide(mcsat_solver_t* mcsat) {
     // the decided score
     assert(var != variable_null);
     double var_score = var_queue_get_activity(&mcsat->var_queue, var);
-    for (i = 0; i < skipped_variables.size; ++ i) {
+    for (uint32_t i = 0; i < skipped_variables.size; ++ i) {
       variable_t skipped_var = skipped_variables.data[i];
       var_queue_set_activity(&mcsat->var_queue, skipped_var, var_score);
       var_queue_insert(&mcsat->var_queue, skipped_var);
@@ -2551,7 +2624,7 @@ void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_fi
     assert(x_value >= 0);
     trail_add_propagation(mcsat->trail, x_var, &value, plugin_i, mcsat->trail->decision_level);
     mcsat_value_destruct(&value);
-    mcsat_process_registeration_queue(mcsat);
+    mcsat_process_registration_queue(mcsat);
   }
 
   mcsat_pop(mcsat);
@@ -2584,7 +2657,7 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin
       // Make sure the variable is registered (maybe it doesn't appear in assertions)
       variable_t x_var = variable_db_get_variable(mcsat->var_db, unsigned_term(x));
       ivector_push(&mcsat->assumption_vars, x_var);
-      mcsat_process_registeration_queue(mcsat);
+      mcsat_process_registration_queue(mcsat);
     }
   }
 
@@ -2703,6 +2776,7 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin
       break;
     }
 
+    // update the variable selection heuristic
     var_queue_decay_activities(&mcsat->var_queue);
   }
 
@@ -2714,7 +2788,7 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin
   }
 
   // Make sure any additional terms are registered
-  mcsat_process_registeration_queue(mcsat);
+  mcsat_process_registration_queue(mcsat);
 
 solve_done:
 
diff --git a/src/mcsat/variable_queue.c b/src/mcsat/variable_queue.c
index d56b64926..17c042e90 100644
--- a/src/mcsat/variable_queue.c
+++ b/src/mcsat/variable_queue.c
@@ -114,13 +114,13 @@ void var_queue_update_up(var_queue_t *queue, variable_t x, uint32_t i) {
 }
 
 static
-void var_queue_update_down(var_queue_t *queue) {
+void var_queue_update_down(var_queue_t *queue, uint32_t i) {
   double *act;
   int32_t *index;
   variable_t *h;
   variable_t x, y, z;
   double ax, ay, az;
-  uint32_t i, j, last;
+  uint32_t j, last;
 
   last = queue->heap_last;
   queue->heap_last = last - 1;
@@ -128,6 +128,7 @@ void var_queue_update_down(var_queue_t *queue) {
     assert(queue->heap_last == 0);
     return;
   }
+  assert(i <= last);
 
   h = queue->heap;
   index = queue->heap_index;
@@ -137,8 +138,7 @@ void var_queue_update_down(var_queue_t *queue) {
   h[last] = -2;  // set end marker: act[-2] is negative
   az = act[z];   // activity of the last element
 
-  i = 1;      // root
-  j = 2;      // left child of i
+  j = i << 1;    // left child of i
   while (j < last) {
     /*
      * find child of i with highest activity.
@@ -204,11 +204,20 @@ variable_t var_queue_pop(var_queue_t *queue) {
   queue->heap_index[top] = -1;
 
   // repair the heap
-  var_queue_update_down(queue);
+  var_queue_update_down(queue, 1);
 
   return top;
 }
 
+void var_queue_remove(var_queue_t *queue, variable_t var) {
+  if (queue->heap_index[var] >= 0) {
+    uint32_t idx = queue->heap_index[var];
+    assert(idx <= queue->heap_last);
+    var_queue_update_down(queue, idx);
+    queue->heap_index[var] = -1;
+  }
+}
+
 /** Get random element (the heap must not be empty) */
 variable_t var_queue_random(var_queue_t *queue, double* seed) {
   assert(queue->heap_last > 0);
diff --git a/src/mcsat/variable_queue.h b/src/mcsat/variable_queue.h
index 484a1ac18..f1d73a97b 100644
--- a/src/mcsat/variable_queue.h
+++ b/src/mcsat/variable_queue.h
@@ -84,6 +84,9 @@ bool var_queue_is_empty(var_queue_t *queue);
 /** Get and remove top element (the heap must not be empty) */
 variable_t var_queue_pop(var_queue_t *queue);
 
+/** Removes one variable from the heap (var must be on the heap) */
+void var_queue_remove(var_queue_t *queue, variable_t var);
+
 /** Get and remove random element (the heap must not be empty) */
 variable_t var_queue_random(var_queue_t *queue, double *seed);
 
diff --git a/src/utils/int_queues.c b/src/utils/int_queues.c
index 600f09ec2..0a3ddca05 100644
--- a/src/utils/int_queues.c
+++ b/src/utils/int_queues.c
@@ -26,24 +26,24 @@
 #include "utils/memalloc.h"
 
 
-/*
- * Initialize a queue of size n
+/**
+ * Initialize a queue of capacity n
  */
 void init_int_queue(int_queue_t *q, uint32_t n) {
   if (n == 0) {
-    n = DEFAULT_INT_QUEUE_INITIAL_SIZE;
-  } else if (n > MAX_INT_QUEUE_SIZE) {
+    n = DEFAULT_INT_QUEUE_INITIAL_CAPACITY;
+  } else if (n > MAX_INT_QUEUE_CAPACITY) {
     out_of_memory();
   }
 
   q->data = (int32_t *) safe_malloc(n * sizeof(int32_t));
-  q->size = n;
+  q->capacity = n;
   q->head = 0;
   q->tail = 0;
 }
 
 
-/*
+/**
  * Delete: free data array
  */
 void delete_int_queue(int_queue_t *q) {
@@ -51,28 +51,26 @@ void delete_int_queue(int_queue_t *q) {
   q->data = NULL;
 }
 
-
-/*
+/**
  * Resize the queue. make data array 50% larger.
  * content of data array is unchanged
  */
-static void resize_queue(int_queue_t *q) {
+static
+void resize_queue(int_queue_t *q) {
   uint32_t n;
 
-  n = q->size + 1;
+  n = q->capacity + 1;
   n += n >> 1;
 
-  if (n > MAX_INT_QUEUE_SIZE) {
+  if (n > MAX_INT_QUEUE_CAPACITY) {
     out_of_memory();
   }
 
   q->data = (int32_t *) safe_realloc(q->data, n * sizeof(int32_t));
-  q->size = n;
+  q->capacity = n;
 }
 
-
-
-/*
+/**
  * Push element x at the end of the queue
  */
 void int_queue_push(int_queue_t *q, int32_t x) {
@@ -83,7 +81,7 @@ void int_queue_push(int_queue_t *q, int32_t x) {
   i ++;
   q->tail = i;
 
-  if (i == q->size) {
+  if (i == q->capacity) {
     if (q->head == 0) {
       /*
        * full queue, stored in data[0...size-1],
@@ -99,9 +97,9 @@ void int_queue_push(int_queue_t *q, int32_t x) {
      * increase the size and shift data[head .. size - 1] to the end
      * of the new data array.
      */
-    n = q->size;
+    n = q->capacity;
     resize_queue(q);
-    j = q->size;
+    j = q->capacity;
     do {
       n --;
       j --;
@@ -111,8 +109,7 @@ void int_queue_push(int_queue_t *q, int32_t x) {
   }
 }
 
-
-/*
+/**
  * Push a[0 ... n-1] in the queue (in this order)
  */
 void int_queue_push_array(int_queue_t *q, int32_t *a, uint32_t n) {
@@ -123,8 +120,7 @@ void int_queue_push_array(int_queue_t *q, int32_t *a, uint32_t n) {
   }
 }
 
-
-/*
+/**
  * Return first element and remove it
  */
 int32_t int_queue_pop(int_queue_t *q) {
@@ -136,34 +132,63 @@ int32_t int_queue_pop(int_queue_t *q) {
   h = q->head;
   x = q->data[h];
   h ++;
-  if (h >= q->size) h = 0;
+  if (h >= q->capacity) h = 0;
   q->head = h;
 
   return x;
 }
 
-
-
-/*
+/**
  * Get the first element (don't remove it).
  */
-int32_t int_queue_first(int_queue_t *q) {
+int32_t int_queue_first(const int_queue_t *q) {
   assert(q->head != q->tail);
   return q->data[q->head];
 }
 
-
-/*
+/**
  * Get the last element (don't remove it)
  */
-int32_t int_queue_last(int_queue_t *q) {
+int32_t int_queue_last(const int_queue_t *q) {
   uint32_t i;
 
   assert(q->head != q->tail);
   i = q->tail;
   if (i == 0) {
-    i = q->size;
+    i = q->capacity;
   }
   assert(i > 0);
   return q->data[i-1];
 }
+
+/**
+ * Get element at position i
+ */
+int32_t int_queue_at(const int_queue_t *q, uint32_t i) {
+  assert(q->head != q->tail);
+
+  if (q->head < q->tail) {
+    assert(q->head + i < q->tail);
+    return q->data[q->head + i];
+  } else if (q->head > q->tail) {
+    uint32_t size_first = q->capacity - q->head;
+    assert(i < size_first || i - size_first < q->tail);
+    return i < size_first
+      ? q->data[q->head + i]
+      : q->data[i - size_first];
+  }
+
+  assert(false);
+  return 0;
+}
+
+/**
+ * Get size of queue
+ */
+uint32_t int_queue_size(const int_queue_t *q) {
+  if (q->head <= q->tail) {
+    return q->tail - q->head;
+  } else {
+    return (q->capacity - q->head) + q->tail;
+  }
+}
diff --git a/src/utils/int_queues.h b/src/utils/int_queues.h
index 9d916c72f..91a25203b 100644
--- a/src/utils/int_queues.h
+++ b/src/utils/int_queues.h
@@ -27,97 +27,110 @@
 #include <stdbool.h>
 
 
-/*
+/**
  * Components:
  * - data = integer array to store the elements
- * - size = size of that array
+ * - capacity = size of that array
  * - head, tail = indices between 0 and size - 1.
  * The queue is managed as a circular array:
  * - if head = tail, the queue is empty
  * - if head < tail, the queue content is data[head ... tail-1]
  * - if head > tail, the queue content is
- *     data[head...size-1] + data[0 ... tail-1]
+ *     data[head...capacity-1] + data[0 ... tail-1]
  */
 typedef struct int_queue_s {
   int32_t *data;
-  uint32_t size;
+  uint32_t capacity;
   uint32_t head;
   uint32_t tail;
 } int_queue_t;
 
 
-/*
+/**
  * Maximal size: make sure n * sizeof(int32_t) does not overflow
  */
-#define MAX_INT_QUEUE_SIZE (UINT32_MAX/sizeof(int32_t))
+#define MAX_INT_QUEUE_CAPACITY (UINT32_MAX/sizeof(int32_t))
 
 
-/*
+/**
  * Default size
  */
-#define DEFAULT_INT_QUEUE_INITIAL_SIZE 16
+#define DEFAULT_INT_QUEUE_INITIAL_CAPACITY 16
 
 
-/*
+/**
  * Initialize a queue of size n.
  * If n = 0 then DEFAULT_QUEUE_INITIAL_SIZE is used.
  */
-extern void init_int_queue(int_queue_t *q, uint32_t n);
+void init_int_queue(int_queue_t *q, uint32_t n);
 
 
-/*
+/**
  * Delete q
  */
-extern void delete_int_queue(int_queue_t *q);
+void delete_int_queue(int_queue_t *q);
 
 
-/*
+/**
  * Push element x in the queue (at the end)
  */
-extern void int_queue_push(int_queue_t *q, int32_t x);
+void int_queue_push(int_queue_t *q, int32_t x);
 
 
-/*
+/**
  * Push a[0 ... n-1] in the queue (in this order)
  */
-extern void int_queue_push_array(int_queue_t *q, int32_t *a, uint32_t n);
+void int_queue_push_array(int_queue_t *q, int32_t *a, uint32_t n);
 
 
-/*
+/**
  * Check whether the queue is empty
  */
 static inline bool int_queue_is_empty(int_queue_t *q) {
   return q->head == q->tail;
 }
 
-/*
+
+/**
+ * Gets the size of the queue.
+ */
+uint32_t int_queue_size(const int_queue_t *q);
+
+
+/**
  * Return the first element and remove it from q.
  * - q must be non-empty.
  */
-extern int32_t int_queue_pop(int_queue_t *q);
+int32_t int_queue_pop(int_queue_t *q);
 
 
-/*
+/**
  * Get the first element of q but don't remove it.
  * - q must be non-empty
  */
-extern int32_t int_queue_first(int_queue_t *q);
+int32_t int_queue_first(const int_queue_t *q);
 
 
-/*
+/**
  * Get the last element of q (don't remove it)
  * - q must be non-empty
  */
-extern int32_t int_queue_last(int_queue_t *q);
+int32_t int_queue_last(const int_queue_t *q);
 
 
-/*
+/**
+ * Gets the element at position i
+ */
+int32_t int_queue_at(const int_queue_t *q, uint32_t i);
+
+
+/**
  * Empty the queue
  */
-static inline void int_queue_reset(int_queue_t *q) {
+static inline
+void int_queue_reset(int_queue_t *q) {
   q->head = 0;
   q->tail = 0;
 }
 
-
 #endif /* __INT_QUEUES_H */
diff --git a/tests/regress/mcsat/nra/issue204.smt2.options b/tests/regress/mcsat/nra/issue204.smt2.options
new file mode 100644
index 000000000..55e9392b3
--- /dev/null
+++ b/tests/regress/mcsat/nra/issue204.smt2.options
@@ -0,0 +1 @@
+--mcsat --mcsat-nra-bound
\ No newline at end of file
diff --git a/tests/regress/mcsat/uf/assumptions/issue274.smt2.gold b/tests/regress/mcsat/uf/assumptions/issue274.smt2.gold
index ea078ecf1..34805e86a 100644
--- a/tests/regress/mcsat/uf/assumptions/issue274.smt2.gold
+++ b/tests/regress/mcsat/uf/assumptions/issue274.smt2.gold
@@ -1,2 +1,2 @@
 unsat
-(or (= r1 0) (>= (* -1 r1) 0) (>= (+ -6873817 (* -35151836873817 r1) (* -10000000 (^ r1 2))) 0) (>= (+ -35151836873817 (* -20000000 r1)) 0))
+(or (= r1 0) (>= (* -1 r1) 0) )