diff --git a/src/mcsat/nra/feasible_set_db.c b/src/mcsat/nra/feasible_set_db.c
index 184655122..509fc7946 100644
--- a/src/mcsat/nra/feasible_set_db.c
+++ b/src/mcsat/nra/feasible_set_db.c
@@ -674,3 +674,15 @@ variable_t feasible_set_db_get_fixed(feasible_set_db_t* db) {
   }
   return variable_null;
 }
+
+void feasible_set_db_approximate_value(feasible_set_db_t* db, variable_t constraint_var, lp_interval_t* result) {
+  lp_feasibility_set_t* feasible = feasible_set_db_get(db, constraint_var);
+  if (feasible != NULL) {
+    lp_feasibility_set_to_interval(feasible, result);
+  } else {
+    lp_interval_t full;
+    lp_interval_construct_full(&full);
+    lp_interval_swap(&full, result);
+    lp_interval_destruct(&full);
+  }
+}
diff --git a/src/mcsat/nra/feasible_set_db.h b/src/mcsat/nra/feasible_set_db.h
index 37d82e794..432f67843 100644
--- a/src/mcsat/nra/feasible_set_db.h
+++ b/src/mcsat/nra/feasible_set_db.h
@@ -69,3 +69,6 @@ variable_t feasible_set_db_get_cheap_unassigned(feasible_set_db_t* db, lp_value_
 
 /** Marks all the top level reasons */
 void feasible_set_db_gc_mark(feasible_set_db_t* db, gc_info_t* gc_vars);
+
+/** Get an interval approximation of the value */
+void feasible_set_db_approximate_value(feasible_set_db_t* db, variable_t constraint_var, lp_interval_t* result);
diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c
index a2bfb0e1d..85b83da6f 100644
--- a/src/mcsat/nra/nra_plugin.c
+++ b/src/mcsat/nra/nra_plugin.c
@@ -118,13 +118,12 @@ void nra_plugin_construct(plugin_t* plugin, plugin_context_t* ctx) {
   nra->lp_data.lp_var_order_size = 0;
   nra->lp_data.lp_ctx = lp_polynomial_context_new(lp_Z, nra->lp_data.lp_var_db, nra->lp_data.lp_var_order);
   nra->lp_data.lp_assignment = lp_assignment_new(nra->lp_data.lp_var_db);
+  nra->lp_data.lp_interval_assignment = lp_interval_assignment_new(nra->lp_data.lp_var_db);
 
   // Tracing in libpoly
   if (false) {
-    lp_trace_enable("coefficient");
-    lp_trace_enable("coefficient::roots");
-    lp_trace_enable("polynomial");
-    lp_trace_enable("polynomial::check_input");
+    lp_trace_enable("coefficient::interval");
+    lp_trace_enable("polynomial::bounds");
   }
 
   // Trace pscs
@@ -206,6 +205,7 @@ void nra_plugin_destruct(plugin_t* plugin) {
   lp_variable_order_detach(nra->lp_data.lp_var_order);
   lp_variable_db_detach(nra->lp_data.lp_var_db);
   lp_assignment_delete(nra->lp_data.lp_assignment);
+  lp_interval_assignment_delete(nra->lp_data.lp_interval_assignment);
 
   delete_rba_buffer(&nra->buffer);
 }
@@ -676,6 +676,72 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop)
   int_mset_destruct(&t_variables);
 }
 
+static
+void nra_plugin_infer_bounds_from_constraint(nra_plugin_t* nra, trail_token_t* prop, variable_t constraint_var) {
+
+  uint32_t i;
+
+  // Just at base level for now
+  if (!trail_is_at_base_level(nra->ctx->trail)) {
+    return;
+  }
+
+  if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) {
+    ctx_trace_printf(nra->ctx, "nra infer bounds: constraint :\n");
+    ctx_trace_term(nra->ctx, variable_db_get_term(nra->ctx->var_db, constraint_var));
+  }
+
+  // Get the constraint
+  const poly_constraint_t* constraint = poly_constraint_db_get(nra->constraint_db, constraint_var);
+
+  // We don't handle root constraints
+  if (poly_constraint_is_root_constraint(constraint)) {
+    return;
+  }
+
+  // Value of the constraint in the trail
+  bool trail_value = trail_get_boolean_value(nra->ctx->trail, constraint_var);
+
+  // Potentially inferred variables
+  ivector_t lp_variables;
+  init_ivector(&lp_variables, 0);
+
+  // Compute the bounds
+  lp_interval_assignment_t* m = nra->lp_data.lp_interval_assignment;
+  lp_interval_assignment_reset(m);
+  bool conflict = poly_constraint_infer_bounds(constraint, !trail_value, m, &lp_variables);
+  if (conflict) {
+    if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) {
+      ctx_trace_printf(nra->ctx, "nra infer bounds: conflict\n");
+    }
+    nra_plugin_report_conflict(nra, prop, constraint_var);
+  } else {
+    if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) {
+      ctx_trace_printf(nra->ctx, "nra infer bounds: learned :\n");
+      lp_interval_assignment_print(m, ctx_trace_out(nra->ctx));
+      ctx_trace_printf(nra->ctx, "\n");
+    }
+
+    // Set the bounds
+    for (i = 0; i < lp_variables.size; ++ i) {
+      lp_variable_t x_lp = lp_variables.data[i];
+      const lp_interval_t* x_interval = lp_interval_assignment_get_interval(m, x_lp);
+      assert(x_interval != NULL);
+      if (!lp_interval_is_full(x_interval)) {
+        variable_t x = nra_plugin_get_variable_from_lp_variable(nra, x_lp);
+        lp_feasibility_set_t* x_feasible = lp_feasibility_set_new_from_interval(x_interval);
+        bool consistent = feasible_set_db_update(nra->feasible_set_db, x, x_feasible, &constraint_var, 1);
+        if (!consistent) {
+          nra_plugin_report_conflict(nra, prop, constraint_var);
+        }
+      }
+    }
+
+    delete_ivector(&lp_variables);
+  }
+}
+
+
 static
 void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, variable_t constraint_var) {
 
@@ -948,9 +1014,21 @@ void nra_plugin_propagate(plugin_t* plugin, trail_token_t* prop) {
       // Real variables, detect if the constraint is unit
       nra_plugin_process_variable_assignment(nra, prop, var);
     }
-    if (nra_plugin_get_unit_info(nra, var) == CONSTRAINT_UNIT) {
-      // Process any unit constraints
-      nra_plugin_process_unit_constraint(nra, prop, var);
+    if (nra_plugin_has_unit_info(nra, var)) {
+      constraint_unit_info_t info = nra_plugin_get_unit_info(nra, var);
+      switch (info) {
+      case CONSTRAINT_UNIT:
+        // Process any unit constraints
+        nra_plugin_process_unit_constraint(nra, prop, var);
+        break;
+      case CONSTRAINT_UNKNOWN:
+        // Try to infer any bounds
+        nra_plugin_infer_bounds_from_constraint(nra, prop, var);
+        break;
+      case CONSTRAINT_FULLY_ASSIGNED:
+        // Do nothing
+        break;
+      }
     }
   }
 
@@ -1785,6 +1863,70 @@ void nra_plugin_set_exception_handler(plugin_t* plugin, jmp_buf* handler) {
   nra->exception = handler;
 }
 
+
+static
+void nra_plugin_learn(plugin_t* plugin, trail_token_t* prop) {
+  uint32_t i;
+  variable_t constraint_var;
+
+  nra_plugin_t* nra = (nra_plugin_t*) plugin;
+  const mcsat_trail_t* trail = nra->ctx->trail;
+
+
+  if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) {
+    ctx_trace_printf(nra->ctx, "nra_plugin_learn(): trail = ");
+    trail_print(trail, ctx_trace_out(nra->ctx));
+  }
+
+  // Get constraints at
+  // - constraint_db->constraints
+  const ivector_t* all_constraint_vars = poly_constraint_db_get_constraints(nra->constraint_db);
+  for (i = 0; i < all_constraint_vars->size; ++ i)  {
+    constraint_var = all_constraint_vars->data[i];
+
+    // Check if it has a value already
+    bool has_value = trail_has_value(trail, constraint_var);
+    if (has_value) {
+      if (trail_get_source_id(trail, constraint_var) == nra->ctx->plugin_id) {
+        // No need to re-evaluate already propagated stuff
+        continue;
+      }
+    }
+
+    if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) {
+      ctx_trace_printf(nra->ctx, "nra_plugin_learn(): ");
+      ctx_trace_term(nra->ctx, variable_db_get_term(nra->ctx->var_db, constraint_var));
+    }
+
+    // Approximate the value
+    const mcsat_value_t* constraint_value = poly_constraint_db_approximate(nra->constraint_db, constraint_var, nra);
+    if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) {
+      ctx_trace_printf(nra->ctx, "nra_plugin_learn(): value = ");
+      FILE* out = ctx_trace_out(nra->ctx);
+      if (constraint_value != NULL) {
+        mcsat_value_print(constraint_value, out);
+      } else {
+        fprintf(out, "no value");
+      }
+      fprintf(out, "\n");
+    }
+    if (constraint_value != NULL) {
+      if (has_value) {
+        // Need to check
+        bool existing_value = trail_get_boolean_value(trail, constraint_var);
+        if (existing_value != constraint_value->b) {
+          // Propagates different value, mark conflict
+          nra_plugin_report_conflict(nra, prop, variable_null);
+          break;
+        }
+      } else {
+        prop->add(prop, constraint_var, constraint_value);
+      }
+    }
+  }
+
+}
+
 plugin_t* nra_plugin_allocator(void) {
   nra_plugin_t* plugin = safe_malloc(sizeof(nra_plugin_t));
   plugin_construct((plugin_t*) plugin);
@@ -1795,6 +1937,7 @@ plugin_t* nra_plugin_allocator(void) {
   plugin->plugin_interface.event_notify        = nra_plugin_event_notify;
   plugin->plugin_interface.propagate           = nra_plugin_propagate;
   plugin->plugin_interface.decide              = nra_plugin_decide;
+  plugin->plugin_interface.learn               = nra_plugin_learn;
   plugin->plugin_interface.get_conflict        = nra_plugin_get_conflict;
   plugin->plugin_interface.explain_propagation = nra_plugin_explain_propagation;
   plugin->plugin_interface.explain_evaluation  = nra_plugin_explain_evaluation;
diff --git a/src/mcsat/nra/nra_plugin_explain.c b/src/mcsat/nra/nra_plugin_explain.c
index 2eb7d9393..7f6bcec65 100644
--- a/src/mcsat/nra/nra_plugin_explain.c
+++ b/src/mcsat/nra/nra_plugin_explain.c
@@ -1017,6 +1017,26 @@ void nra_plugin_explain_conflict(nra_plugin_t* nra, const int_mset_t* pos, const
     int_mset_destruct(&variables);
   }
 
+  // Check if there is a simple Fourier-Motzkin explanation
+  if (false && core->size == 2 && lemma_reasons->size == 0) {
+    variable_t c0_var = core->data[0];
+    variable_t c1_var = core->data[1];
+    bool c0_negated = !constraint_get_value(nra->ctx->trail, pos, neg, c0_var);
+    bool c1_negated = !constraint_get_value(nra->ctx->trail, pos, neg, c1_var);
+    const poly_constraint_t* c0 = poly_constraint_db_get(nra->constraint_db, c0_var);
+    const poly_constraint_t* c1 = poly_constraint_db_get(nra->constraint_db, c1_var);
+    bool resolved = poly_constraint_resolve_fm(c0, c0_negated, c1, c1_negated, nra, conflict);
+    if (resolved) {
+      term_t c0_term = variable_db_get_term(nra->ctx->var_db, c0_var);
+      if (c0_negated) c0_term = opposite_term(c0_term);
+      term_t c1_term = variable_db_get_term(nra->ctx->var_db, c1_var);
+      if (c1_negated) c1_term = opposite_term(c1_term);
+      ivector_push(conflict, c0_term);
+      ivector_push(conflict, c1_term);
+      return;
+    }
+  }
+
   // Create the map from variables to
   lp_projection_map_t projection_map;
   lp_projection_map_construct(&projection_map, nra);
@@ -1027,8 +1047,20 @@ void nra_plugin_explain_conflict(nra_plugin_t* nra, const int_mset_t* pos, const
     variable_t constraint_var = core->data[core_i];
     assert(constraint_has_value(nra->ctx->trail, pos, neg, constraint_var));
     const poly_constraint_t* constraint = poly_constraint_db_get(nra->constraint_db, constraint_var);
-    const lp_polynomial_t* p = poly_constraint_get_polynomial(constraint);
-    lp_projection_map_add(&projection_map, p);
+    // If the polynomial isn't unit, it is a global inference, so we explain with a different polynomial
+    if (!poly_constraint_is_unit(constraint, nra->lp_data.lp_assignment)) {
+      const lp_polynomial_t* p = poly_constraint_get_polynomial(constraint);
+      lp_sign_condition_t sgn_condition = poly_constraint_get_sign_condition(constraint);
+      bool negated = !trail_get_boolean_value(nra->ctx->trail, constraint_var);
+      lp_variable_t x = poly_constraint_get_top_variable(constraint);
+      lp_polynomial_t* p_inference_reason = lp_polynomial_constraint_explain_infer_bounds(p, sgn_condition, negated, x);
+      lp_projection_map_add(&projection_map, p_inference_reason);
+      lp_polynomial_delete(p_inference_reason);
+    } else {
+      const lp_polynomial_t* p = poly_constraint_get_polynomial(constraint);
+      lp_projection_map_add(&projection_map, p);
+    }
+
   }
 
   // Add all the top-level reasons for the conflict variable
diff --git a/src/mcsat/nra/nra_plugin_internal.c b/src/mcsat/nra/nra_plugin_internal.c
index 3596aa7ff..0cb396e35 100644
--- a/src/mcsat/nra/nra_plugin_internal.c
+++ b/src/mcsat/nra/nra_plugin_internal.c
@@ -154,6 +154,11 @@ void nra_plugin_set_unit_info(nra_plugin_t* nra, variable_t constraint, variable
   }
 }
 
+bool nra_plugin_has_unit_info(const nra_plugin_t* nra, variable_t constraint) {
+  int_hmap_pair_t* find = int_hmap_find(&((nra_plugin_t*)nra)->constraint_unit_info, constraint);
+  return find != NULL;
+}
+
 constraint_unit_info_t nra_plugin_get_unit_info(nra_plugin_t* nra, variable_t constraint) {
   int_hmap_pair_t* find = int_hmap_find(&nra->constraint_unit_info, constraint);
   if (find == NULL)  {
diff --git a/src/mcsat/nra/nra_plugin_internal.h b/src/mcsat/nra/nra_plugin_internal.h
index f9b64651d..cadfc4c54 100644
--- a/src/mcsat/nra/nra_plugin_internal.h
+++ b/src/mcsat/nra/nra_plugin_internal.h
@@ -102,6 +102,8 @@ struct nra_plugin_s {
     lp_polynomial_context_t* lp_ctx;
     /** Libpoly model */
     lp_assignment_t* lp_assignment;
+    /** Interval assignment for bound inference */
+    lp_interval_assignment_t* lp_interval_assignment;
 
     /** Map from libpoly variables to mcsat variables */
     int_hmap_t lp_to_mcsat_var_map;
@@ -160,6 +162,9 @@ variable_t nra_plugin_get_variable_from_lp_variable(nra_plugin_t* nra, lp_variab
 /** Set the unit info for the given constraint */
 void nra_plugin_set_unit_info(nra_plugin_t* nra, variable_t constraint, variable_t unit_var, constraint_unit_info_t value);
 
+/** Are we tracking this constraint */
+bool nra_plugin_has_unit_info(const nra_plugin_t* nra, variable_t constraint);
+
 /** Get the unit info for the given constraint */
 constraint_unit_info_t nra_plugin_get_unit_info(nra_plugin_t* nra, variable_t constraint);
 
diff --git a/src/mcsat/nra/poly_constraint.c b/src/mcsat/nra/poly_constraint.c
index 42c52b548..85b3b5fc4 100644
--- a/src/mcsat/nra/poly_constraint.c
+++ b/src/mcsat/nra/poly_constraint.c
@@ -24,6 +24,9 @@
 #include <poly/variable_db.h>
 #include <poly/variable_list.h>
 #include <poly/feasibility_set.h>
+#include <poly/interval.h>
+#include <poly/assignment.h>
+#include <poly/polynomial_vector.h>
 
 /**
  * A constraint of the form sgn(p(x)) = sgn_conition.
@@ -69,6 +72,9 @@ struct poly_constraint_db_struct {
 
   /** Map from variables to constraint references */
   int_hmap_t var_to_constraint_map;
+
+  /** List of all constraint variables */
+  ivector_t all_constraint_variables;
 };
 
 static
@@ -117,10 +123,11 @@ void poly_constraint_db_gc_sweep(poly_constraint_db_t* db, const gc_info_t* gc_v
   init_int_hmap(&new_var_to_constraint_map, 0);
 
   // Move the constraints
-  int_hmap_pair_t* it = int_hmap_first_record(&db->var_to_constraint_map);
-  for (; it != NULL; it = int_hmap_next_record(&db->var_to_constraint_map, it)) {
+  uint32_t i, to_keep = 0;
+  for (i = 0; i < db->all_constraint_variables.size; ++ i) {
+    variable_t old_constraint_var = db->all_constraint_variables.data[i];
+    int_hmap_pair_t* it = int_hmap_find(&db->var_to_constraint_map, old_constraint_var);
     // Do we keep it
-    variable_t old_constraint_var = it->key;
     variable_t new_constraint_var = gc_info_get_reloc(gc_vars, old_constraint_var);
     poly_constraint_t* constraint = db->constraints.data[it->val];
     if (new_constraint_var != gc_vars->null_value) {
@@ -128,6 +135,7 @@ void poly_constraint_db_gc_sweep(poly_constraint_db_t* db, const gc_info_t* gc_v
       uint32_t new_index = new_constraints.size;
       pvector_push(&new_constraints, constraint);
       int_hmap_add(&new_var_to_constraint_map, new_constraint_var, new_index);
+      db->all_constraint_variables.data[to_keep ++] = new_constraint_var;
     } else {
       if (ctx_trace_enabled(db->nra->ctx, "nra::gc")) {
         ctx_trace_printf(db->nra->ctx, "Removing constraint :");
@@ -144,6 +152,7 @@ void poly_constraint_db_gc_sweep(poly_constraint_db_t* db, const gc_info_t* gc_v
   delete_int_hmap(&db->var_to_constraint_map);
   db->constraints = new_constraints;
   db->var_to_constraint_map = new_var_to_constraint_map;
+  ivector_shrink(&db->all_constraint_variables, to_keep);
 }
 
 
@@ -278,6 +287,149 @@ lp_feasibility_set_t* poly_constraint_get_feasible_set(const poly_constraint_t*
   return feasible;
 }
 
+bool poly_constraint_infer_bounds(const poly_constraint_t* cstr, bool negated, lp_interval_assignment_t* m, ivector_t* inferred_vars) {
+
+  // TODO: is it possible to support root constraints
+  if (poly_constraint_is_root_constraint(cstr)) {
+    return false;
+  }
+
+  // Infer some bounds
+  int inference_result = lp_polynomial_constraint_infer_bounds(cstr->polynomial, cstr->sgn_condition, negated, m);
+  if (inference_result == 0) {
+    return false;
+  }
+  if (inference_result == -1) {
+    return true;
+  }
+
+  lp_variable_list_t vars;
+  lp_variable_list_construct(&vars);
+  lp_polynomial_get_variables(cstr->polynomial, &vars);
+  uint32_t var_i;
+  for (var_i = 0; var_i < vars.list_size; ++ var_i) {
+    lp_variable_t x_lp = vars.list[var_i];
+    const lp_interval_t* x_interval = lp_interval_assignment_get_interval(m, x_lp);
+    if (x_interval != NULL) {
+      // something is inferred
+      ivector_push(inferred_vars, x_lp);
+    }
+  }
+  lp_variable_list_destruct(&vars);
+
+  return false;
+}
+
+bool poly_constraint_resolve_fm(const poly_constraint_t* c0, bool c0_negated, const poly_constraint_t* c1, bool c1_negated, nra_plugin_t* nra, ivector_t* out) {
+
+  lp_polynomial_context_t* ctx = nra->lp_data.lp_ctx;
+  lp_assignment_t* m = nra->lp_data.lp_assignment;
+
+  if (poly_constraint_is_root_constraint(c0) || poly_constraint_is_root_constraint(c1)) {
+    return false;
+  }
+
+  if (ctx_trace_enabled(nra->ctx, "mcsat::nra::explain")) {
+    ctx_trace_printf(nra->ctx, "c0 %s: ", c0_negated ? "(negated)" : "");
+    poly_constraint_print(c0, ctx_trace_out(nra->ctx));
+    ctx_trace_printf(nra->ctx, "\n");
+    ctx_trace_printf(nra->ctx, "c1 %s: ", c1_negated ? "(negated)" : "");
+    poly_constraint_print(c1, ctx_trace_out(nra->ctx));
+    ctx_trace_printf(nra->ctx, "\n");
+  }
+
+  lp_polynomial_vector_t* assumptions = lp_polynomial_vector_new(ctx);
+
+  lp_sign_condition_t R_sgn_condition;
+  lp_polynomial_t* R = lp_polynomial_new(ctx);
+  lp_sign_condition_t c0_sgn_condition = c0_negated ? lp_sign_condition_negate(c0->sgn_condition) : c0->sgn_condition;
+  lp_sign_condition_t c1_sgn_condition = c1_negated ? lp_sign_condition_negate(c1->sgn_condition) : c1->sgn_condition;
+  bool ok = lp_polynomial_constraint_resolve_fm(c0->polynomial, c0_sgn_condition, c1->polynomial, c1_sgn_condition, m, R, &R_sgn_condition, assumptions);
+  if (ok) {
+    // (C1 && C2 && assumptions && !(p R2 0)) => false
+    term_manager_t* tm = nra->ctx->tm;
+    size_t n = lp_polynomial_vector_size(assumptions);
+    size_t i;
+    for (i = 0; i < n; ++ i) {
+      lp_polynomial_t* assumption_p_i = lp_polynomial_vector_at(assumptions, i);
+      term_t assumption_i_p_term = lp_polynomial_to_yices_term(nra, assumption_p_i);
+      int assumption_i_p_sgn = lp_polynomial_sgn(assumption_p_i, m);
+      term_t assumption_i = NULL_TERM;
+      if (assumption_i_p_sgn < 0) {
+        assumption_i = mk_arith_term_lt0(tm, assumption_i_p_term);
+      } else if (assumption_i_p_sgn > 0) {
+        assumption_i = mk_arith_term_gt0(tm, assumption_i_p_term);
+      } else {
+        assumption_i = mk_arith_term_eq0(tm, assumption_i_p_term);
+      }
+      if (ctx_trace_enabled(nra->ctx, "mcsat::nra::explain")) {
+        ctx_trace_printf(nra->ctx, "adding FM assumption: ");
+        ctx_trace_term(nra->ctx, assumption_i);
+      }
+      ivector_push(out, assumption_i);
+      lp_polynomial_delete(assumption_p_i);
+    }
+    term_t R_p_term = lp_polynomial_to_yices_term(nra, R);
+    term_t R_term = NULL_TERM;
+    switch (R_sgn_condition) {
+    case LP_SGN_LT_0:
+      R_term = mk_arith_term_lt0(tm, R_p_term);
+      break;
+    case LP_SGN_LE_0:
+      R_term = mk_arith_term_leq0(tm, R_p_term);
+      break;
+    case LP_SGN_EQ_0:
+      R_term = mk_arith_term_eq0(tm, R_p_term);
+      break;
+    case LP_SGN_NE_0:
+      R_term = mk_arith_term_neq0(tm, R_p_term);
+      break;
+    case LP_SGN_GT_0:
+      R_term = mk_arith_term_gt0(tm, R_p_term);
+      break;
+    case LP_SGN_GE_0:
+      R_term = mk_arith_term_geq0(tm, R_p_term);
+      break;
+    }
+    R_term = opposite_term(R_term);
+    if (ctx_trace_enabled(nra->ctx, "mcsat::nra::explain")) {
+      ctx_trace_printf(nra->ctx, "adding resolvent: ");
+      ctx_trace_term(nra->ctx, R_term);
+    }
+    ivector_push(out, R_term);
+  }
+
+  lp_polynomial_delete(R);
+  lp_polynomial_vector_delete(assumptions);
+
+  return ok;
+}
+
+
+bool poly_constraint_is_unit(const poly_constraint_t* cstr, const lp_assignment_t* M) {
+  lp_variable_t x = lp_polynomial_top_variable(cstr->polynomial);
+  if (lp_assignment_get_value(M, x)->type != LP_VALUE_NONE) {
+    return false;
+  }
+
+  bool result = true;
+
+  lp_variable_list_t vars;
+  lp_variable_list_construct(&vars);
+  lp_polynomial_get_variables(cstr->polynomial, &vars);
+  uint32_t var_i;
+  for (var_i = 0; var_i < vars.list_size; ++ var_i) {
+    lp_variable_t x_lp = vars.list[var_i];
+    if (x_lp != x && lp_assignment_get_value(M, x_lp)->type == LP_VALUE_NONE) {
+      result = false;
+      break;
+    }
+  }
+  lp_variable_list_destruct(&vars);
+
+  return result;
+}
+
 lp_variable_t poly_constraint_get_top_variable(const poly_constraint_t* cstr) {
   return lp_polynomial_top_variable(cstr->polynomial);
 }
@@ -287,6 +439,7 @@ void poly_constraint_db_construct(poly_constraint_db_t* db, nra_plugin_t* nra) {
 
   init_pvector(&db->constraints, 0);
   init_int_hmap(&db->var_to_constraint_map, 0);
+  init_ivector(&db->all_constraint_variables, 0);
 }
 
 poly_constraint_db_t* poly_constraint_db_new(nra_plugin_t* nra) {
@@ -307,6 +460,7 @@ void poly_constraint_db_destruct(poly_constraint_db_t* db) {
 
   delete_pvector(&db->constraints);
   delete_int_hmap(&db->var_to_constraint_map);
+  delete_ivector(&db->all_constraint_variables);
 }
 
 void poly_constraint_db_delete(poly_constraint_db_t* db) {
@@ -314,6 +468,11 @@ void poly_constraint_db_delete(poly_constraint_db_t* db) {
   safe_free(db);
 }
 
+const ivector_t* poly_constraint_db_get_constraints(const poly_constraint_db_t* db) {
+  return &db->all_constraint_variables;
+}
+
+
 bool poly_constraint_db_check(const poly_constraint_db_t* db) {
   uint32_t i;
   for (i = 0; i < db->constraints.size; ++ i) {
@@ -494,6 +653,7 @@ void poly_constraint_db_add(poly_constraint_db_t* db, variable_t constraint_var)
   // Add the constraint
   pvector_push(&db->constraints, cstr);
   int_hmap_add(&db->var_to_constraint_map, constraint_var, index);
+  ivector_push(&db->all_constraint_variables, constraint_var);
 
   // assert(poly_constraint_db_check(db));
 }
@@ -525,3 +685,53 @@ bool poly_constraint_evaluate(const poly_constraint_t* cstr, nra_plugin_t* nra,
 
   return true;
 }
+
+const mcsat_value_t* poly_constraint_db_approximate(poly_constraint_db_t* db, variable_t constraint_var, nra_plugin_t* nra) {
+  const mcsat_value_t* result = NULL;
+
+  // Get the constraints
+  const poly_constraint_t* cstr = poly_constraint_db_get(db, constraint_var);
+  if (poly_constraint_is_root_constraint(cstr)) {
+    // TODO: check if possible
+    return NULL;
+  }
+
+  // Reset the interval assignment
+  lp_interval_assignment_t* m = nra->lp_data.lp_interval_assignment;
+  lp_interval_assignment_reset(m);
+
+  // Setup the assignment x -> I(x)
+  lp_variable_list_t vars;
+  lp_variable_list_construct(&vars);
+  lp_polynomial_get_variables(cstr->polynomial, &vars);
+  uint32_t var_i;
+  for (var_i = 0; var_i < vars.list_size; ++ var_i) {
+    lp_variable_t x_lp = vars.list[var_i];
+    variable_t x = nra_plugin_get_variable_from_lp_variable(nra, x_lp);
+    lp_interval_t x_interval;
+    lp_interval_construct_full(&x_interval);
+    feasible_set_db_approximate_value(nra->feasible_set_db, x, &x_interval);
+    lp_interval_assignment_set_interval(m, x_lp, &x_interval);
+    lp_interval_destruct(&x_interval);
+  }
+
+  // Evaluate the polynomial
+  lp_interval_t value;
+  lp_interval_construct_full(&value);
+  lp_polynomial_interval_value(cstr->polynomial, m, &value);
+
+  lp_sign_condition_t pos = cstr->sgn_condition;
+  lp_sign_condition_t neg = lp_sign_condition_negate(cstr->sgn_condition);
+
+  if (lp_sign_condition_consistent_interval(pos, &value)) {
+    result = &mcsat_value_true;
+  } else if (lp_sign_condition_consistent_interval(neg, &value)) {
+    result = &mcsat_value_false;
+  }
+
+  // Remove temps
+  lp_variable_list_destruct(&vars);
+  lp_interval_destruct(&value);
+
+  return result;
+}
diff --git a/src/mcsat/nra/poly_constraint.h b/src/mcsat/nra/poly_constraint.h
index e80c20c24..d68cb2d91 100644
--- a/src/mcsat/nra/poly_constraint.h
+++ b/src/mcsat/nra/poly_constraint.h
@@ -1,4 +1,4 @@
-/*
+ /*
  * This file is part of the Yices SMT Solver.
  * Copyright (C) 2017 SRI International.
  *
@@ -52,6 +52,9 @@ void poly_constraint_print_mathematica(const poly_constraint_t* cstr, bool neage
 /** Get the feasible set of the constraint */
 lp_feasibility_set_t* poly_constraint_get_feasible_set(const poly_constraint_t* cstr, const lp_assignment_t* m, bool negated);
 
+/** Infer the bounds for this constraint (inferred_vars are lp_variables). Returns true if conflict detected. */
+bool poly_constraint_infer_bounds(const poly_constraint_t* cstr, bool negated, lp_interval_assignment_t* m, ivector_t* inferred_vars);
+
 /**
  * Is this a valid constraint in the current order.
  */
@@ -83,6 +86,12 @@ lp_variable_t poly_constraint_get_variable(const poly_constraint_t* cstr);
 /** Get the root index (if a root constraint) */
 uint32_t poly_constraint_get_root_index(const poly_constraint_t* cstr);
 
+/** Check if the constraint is unit */
+bool poly_constraint_is_unit(const poly_constraint_t* cstr, const lp_assignment_t* M);
+
+/** Try to resolve the two constraints with Fourier-Motzkin resolution */
+bool poly_constraint_resolve_fm(const poly_constraint_t* c0, bool c0_negated, const poly_constraint_t* c1, bool c1_negated, nra_plugin_t* nra, ivector_t* out);
+
 /** Construct the database */
 void poly_constraint_db_construct(poly_constraint_db_t* db, nra_plugin_t* nra);
 
@@ -95,9 +104,15 @@ void poly_constraint_db_destruct(poly_constraint_db_t* db);
 /** Delete the database */
 void poly_constraint_db_delete(poly_constraint_db_t* db);
 
+/** Get all constraints (as variables) */
+const ivector_t* poly_constraint_db_get_constraints(const poly_constraint_db_t* db);
+
 /** Get the constraint of the variable (must exist) */
 const poly_constraint_t* poly_constraint_db_get(poly_constraint_db_t* db, variable_t constraint_var);
 
+/** Compute an approximation of the constraint value with interval computation */
+const mcsat_value_t* poly_constraint_db_approximate(poly_constraint_db_t* db, variable_t constraint_var, nra_plugin_t* nra);
+
 /** Add a new constraint */
 void poly_constraint_db_add(poly_constraint_db_t* db, variable_t constraint_var);
 
diff --git a/src/mcsat/plugin.h b/src/mcsat/plugin.h
index 5aa3e1dcd..bf6301ed5 100644
--- a/src/mcsat/plugin.h
+++ b/src/mcsat/plugin.h
@@ -214,6 +214,13 @@ struct plugin_s {
    */
   void (*decide) (plugin_t* plugin, variable_t x, trail_token_t* decide, bool must);
 
+  /**
+   * Optional: learn using the given trail token. This is called at base level after
+   * propagation is done and there is no conflict. This is a chance to perform some
+   * more expensive reasoning and propagate consequences.
+   */
+  void (*learn) (plugin_t* plugin, trail_token_t* prop);
+
   /**
    * Explain the conflict that you reported. The plugin should return a conflict
    * such that
@@ -291,6 +298,7 @@ void plugin_construct(plugin_t* plugin) {
   plugin->new_lemma_notify      = NULL;
   plugin->propagate             = NULL;
   plugin->decide                = NULL;
+  plugin->learn                 = NULL;
   plugin->get_conflict          = NULL;
   plugin->explain_propagation   = NULL;
   plugin->explain_evaluation    = NULL;
diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c
index 2c9dc9121..97d88bda1 100644
--- a/src/mcsat/solver.c
+++ b/src/mcsat/solver.c
@@ -1282,7 +1282,7 @@ void mcsat_process_requests(mcsat_solver_t* mcsat) {
  * is encountered.
  */
 static
-bool mcsat_propagate(mcsat_solver_t* mcsat) {
+bool mcsat_propagate(mcsat_solver_t* mcsat, bool run_learning) {
 
   uint32_t plugin_i;
   plugin_t* plugin;
@@ -1295,7 +1295,7 @@ bool mcsat_propagate(mcsat_solver_t* mcsat) {
     // Propagate with all the plugins in turn
     for (plugin_i = 0; trail_is_consistent(mcsat->trail) && plugin_i < mcsat->plugins_count; ++ plugin_i) {
       if (trace_enabled(mcsat->ctx->trace, "mcsat::propagate")) {
-        mcsat_trace_printf(mcsat->ctx->trace, "mcsat_propagate(): with %s\n", mcsat->plugins[plugin_i].plugin_name);
+        mcsat_trace_printf(mcsat->ctx->trace, "mcsat_propagate(): propagting with %s\n", mcsat->plugins[plugin_i].plugin_name);
       }
       // Make the token
       trail_token_construct(&prop_token, mcsat->plugins[plugin_i].plugin_ctx, variable_null);
@@ -1308,6 +1308,25 @@ bool mcsat_propagate(mcsat_solver_t* mcsat) {
         someone_propagated = true;
       }
     }
+    // If at base level, plugins can do some more expensive learning/propagation
+    if (run_learning && !someone_propagated && trail_is_at_base_level(mcsat->trail)) {
+      // Propagate with all the plugins in turn
+      for (plugin_i = 0; trail_is_consistent(mcsat->trail) && plugin_i < mcsat->plugins_count; ++ plugin_i) {
+        if (trace_enabled(mcsat->ctx->trace, "mcsat::propagate")) {
+          mcsat_trace_printf(mcsat->ctx->trace, "mcsat_propagate(): learning with %s\n", mcsat->plugins[plugin_i].plugin_name);
+        }
+        // Make the token
+        trail_token_construct(&prop_token, mcsat->plugins[plugin_i].plugin_ctx, variable_null);
+        // Propagate
+        plugin = mcsat->plugins[plugin_i].plugin;
+        if (plugin->learn) {
+          plugin->learn(plugin, (trail_token_t*) &prop_token);
+        }
+        if (prop_token.used > 0) {
+          someone_propagated = true;
+        }
+      }
+    }
   } while (someone_propagated && trail_is_consistent(mcsat->trail));
 
   return someone_propagated;
@@ -1368,7 +1387,7 @@ void mcsat_assert_formula(mcsat_solver_t* mcsat, term_t f) {
   }
 
   // Do propagation
-  mcsat_propagate(mcsat);
+  mcsat_propagate(mcsat, false);
 }
 
 /**
@@ -1528,7 +1547,7 @@ void mcsat_add_lemma(mcsat_solver_t* mcsat, ivector_t* lemma, term_t decision_bo
   }
 
   // Propagate any
-  mcsat_propagate(mcsat);
+  mcsat_propagate(mcsat, false);
   bool propagated = old_trail_size < mcsat->trail->elements.size;
 
   // Decide a literal if necessary. At this point, if it was UIP they are all
@@ -2036,6 +2055,9 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params) {
   restart_resource = 0;
   luby_init(&luby, mcsat->heuristic_params.restart_interval);
 
+  // Whether to run learning
+  bool learning = true;
+
   while (!mcsat->stop_search) {
 
     // Do we restart
@@ -2049,7 +2071,8 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params) {
     mcsat_process_requests(mcsat);
 
     // Do propagation
-    mcsat_propagate(mcsat);
+    mcsat_propagate(mcsat, learning);
+    learning = false;
 
     // If inconsistent, analyze the conflict
     if (!trail_is_consistent(mcsat->trail)) {
diff --git a/tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2 b/tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2
new file mode 100644
index 000000000..d6ff916be
--- /dev/null
+++ b/tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2
@@ -0,0 +1,27 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :source |
+These benchmarks used in the paper:
+
+  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
+  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
+
+The meti-tarski benchmarks are proof obligations extracted from the
+Meti-Tarski project, see:
+
+  B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover
+  for real-valued special functions. Journal of Automated Reasoning,
+  44(3):175-205, 2010.
+
+Submitted by Dejan Jovanovic for SMT-LIB.
+
+
+|)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun skoC () Real)
+(declare-fun skoS () Real)
+(declare-fun skoX () Real)
+(assert (let ((?v_1 (<= skoX 0)) (?v_0 (* skoC (/ (- 235) 42)))) (and (<= skoS ?v_0) (and (not ?v_1) (and (or (<= ?v_0 skoS) ?v_1) (and (= (* skoS skoS) (+ 1 (* skoC (* skoC (- 1))))) (and (<= skoX 289) (<= 0 skoX))))))))
+(check-sat)
+(exit)
diff --git a/tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2.gold b/tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2.gold
new file mode 100644
index 000000000..6b8a2c3d2
--- /dev/null
+++ b/tests/regress/mcsat/nra/Chua-1-IL-L-chunk-0046.smt2.gold
@@ -0,0 +1 @@
+sat
diff --git a/tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2 b/tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2
new file mode 100644
index 000000000..66d2e7bb9
--- /dev/null
+++ b/tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2
@@ -0,0 +1,28 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :source |
+These benchmarks used in the paper:
+
+  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
+  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
+
+The meti-tarski benchmarks are proof obligations extracted from the
+Meti-Tarski project, see:
+
+  B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover
+  for real-valued special functions. Journal of Automated Reasoning,
+  44(3):175-205, 2010.
+
+Submitted by Dejan Jovanovic for SMT-LIB.
+
+
+|)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun skoSM1 () Real)
+(declare-fun skoSP1 () Real)
+(declare-fun skoS () Real)
+(declare-fun skoX () Real)
+(assert (and (<= (* skoSP1 (+ (* skoSM1 12) (* skoSP1 (* skoSM1 (- 24))))) (* skoSM1 2)) (and (= (+ (- 1) (* skoSP1 skoSP1)) skoX) (and (= (+ 1 (* skoSM1 skoSM1)) skoX) (and (= (* skoS skoS) skoX) (and (not (<= skoX 1)) (and (not (<= skoSP1 0)) (and (not (<= skoSM1 0)) (and (not (<= skoS 0)) (not (<= 5 skoX)))))))))))
+(check-sat)
+(exit)
diff --git a/tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2.gold b/tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2.gold
new file mode 100644
index 000000000..6b8a2c3d2
--- /dev/null
+++ b/tests/regress/mcsat/nra/exp-problem-10-2-chunk-0147.smt2.gold
@@ -0,0 +1 @@
+sat
diff --git a/tests/regress/mcsat/nra/hong_20.smt2 b/tests/regress/mcsat/nra/hong_20.smt2
new file mode 100644
index 000000000..ec7a2955e
--- /dev/null
+++ b/tests/regress/mcsat/nra/hong_20.smt2
@@ -0,0 +1,42 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :source |These benchmarks used in the paper:
+
+  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
+  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
+
+The hong family is a set of crafted benchmarks, a parametrized
+generalization of the problem of Hong, sum x_i^2 < 1 and prod x_i > 1.
+See:
+
+  H. Hong.  Comparison of several decision algorithms for the existential
+  theory of the reals.  1991.
+
+Submitted by Dejan Jovanvic for SMT-LIB.
+|)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x_0 () Real)
+(declare-fun x_1 () Real)
+(declare-fun x_2 () Real)
+(declare-fun x_3 () Real)
+(declare-fun x_4 () Real)
+(declare-fun x_5 () Real)
+(declare-fun x_6 () Real)
+(declare-fun x_7 () Real)
+(declare-fun x_8 () Real)
+(declare-fun x_9 () Real)
+(declare-fun x_10 () Real)
+(declare-fun x_11 () Real)
+(declare-fun x_12 () Real)
+(declare-fun x_13 () Real)
+(declare-fun x_14 () Real)
+(declare-fun x_15 () Real)
+(declare-fun x_16 () Real)
+(declare-fun x_17 () Real)
+(declare-fun x_18 () Real)
+(declare-fun x_19 () Real)
+(assert (< (+ (* x_0 x_0) (+ (* x_1 x_1) (+ (* x_2 x_2) (+ (* x_3 x_3) (+ (* x_4 x_4) (+ (* x_5 x_5) (+ (* x_6 x_6) (+ (* x_7 x_7) (+ (* x_8 x_8) (+ (* x_9 x_9) (+ (* x_10 x_10) (+ (* x_11 x_11) (+ (* x_12 x_12) (+ (* x_13 x_13) (+ (* x_14 x_14) (+ (* x_15 x_15) (+ (* x_16 x_16) (+ (* x_17 x_17) (+ (* x_18 x_18) (* x_19 x_19)))))))))))))))))))) 1))
+(assert (> (* x_0 (* x_1 (* x_2 (* x_3 (* x_4 (* x_5 (* x_6 (* x_7 (* x_8 (* x_9 (* x_10 (* x_11 (* x_12 (* x_13 (* x_14 (* x_15 (* x_16 (* x_17 (* x_18 x_19))))))))))))))))))) 1))
+(check-sat)
+(exit)
diff --git a/tests/regress/mcsat/nra/hong_20.smt2.gold b/tests/regress/mcsat/nra/hong_20.smt2.gold
new file mode 100644
index 000000000..3f65111b0
--- /dev/null
+++ b/tests/regress/mcsat/nra/hong_20.smt2.gold
@@ -0,0 +1 @@
+unsat
diff --git a/tests/regress/mcsat/nra/matrix-1-all-01.smt2 b/tests/regress/mcsat/nra/matrix-1-all-01.smt2
new file mode 100644
index 000000000..e4041df22
--- /dev/null
+++ b/tests/regress/mcsat/nra/matrix-1-all-01.smt2
@@ -0,0 +1,51 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :source |
+From termination analysis of term rewriting.
+
+Submitted by Harald Roman Zankl <Harald.Zankl@uibk.ac.at>
+
+|)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun x6 () Real)
+(declare-fun x13 () Real)
+(declare-fun x3 () Real)
+(declare-fun x10 () Real)
+(declare-fun x0 () Real)
+(declare-fun x17 () Real)
+(declare-fun x7 () Real)
+(declare-fun x14 () Real)
+(declare-fun x4 () Real)
+(declare-fun x11 () Real)
+(declare-fun x1 () Real)
+(declare-fun x18 () Real)
+(declare-fun x8 () Real)
+(declare-fun x15 () Real)
+(declare-fun x5 () Real)
+(declare-fun x12 () Real)
+(declare-fun x2 () Real)
+(declare-fun x9 () Real)
+(declare-fun x16 () Real)
+(assert (>= x6 0))
+(assert (>= x13 0))
+(assert (>= x3 0))
+(assert (>= x10 0))
+(assert (>= x0 0))
+(assert (>= x17 0))
+(assert (>= x7 0))
+(assert (>= x14 0))
+(assert (>= x4 0))
+(assert (>= x11 0))
+(assert (>= x1 0))
+(assert (>= x18 0))
+(assert (>= x8 0))
+(assert (>= x15 0))
+(assert (>= x5 0))
+(assert (>= x12 0))
+(assert (>= x2 0))
+(assert (>= x9 0))
+(assert (>= x16 0))
+(assert (let ((?v_0 (+ x0 (* x2 x3))) (?v_2 (* x2 x4)) (?v_1 (+ x5 (* x6 x7))) (?v_4 (* x12 x3))) (let ((?v_3 (+ (+ x10 (* x11 x3)) ?v_4)) (?v_6 (* x11 x4)) (?v_7 (* x12 x4)) (?v_5 (+ (+ x10 (* x11 x7)) ?v_4))) (let ((?v_17 (and (and (and (and (and (> ?v_0 x0) (>= ?v_0 x0)) (>= ?v_2 x2)) (and (and (and (> ?v_0 ?v_1) (>= ?v_0 ?v_1)) (>= x1 (* x6 x8))) (>= ?v_2 (* x6 x9)))) (and (and (and (> ?v_3 x0) (>= ?v_3 x0)) (>= ?v_6 x1)) (>= ?v_7 x2))) (and (and (and (> ?v_3 ?v_5) (>= ?v_3 ?v_5)) (>= ?v_6 (* x11 x8))) (>= ?v_7 (+ (* x11 x9) ?v_7))))) (?v_8 (+ x13 (* x14 x3))) (?v_9 (+ x7 (* x9 x15))) (?v_11 (+ x13 (* x14 x7))) (?v_10 (+ x7 (* x9 x3))) (?v_13 (* x18 x3))) (let ((?v_12 (+ (+ x16 (* x17 x15)) ?v_13)) (?v_15 (+ x3 (* x4 (+ (+ x16 (* x17 x7)) ?v_13)))) (?v_14 (+ (+ x16 (* x17 x3)) ?v_13)) (?v_16 (* x18 x4))) (and (and (and (and (and (and ?v_17 (and (and (> ?v_8 0) (>= ?v_8 0)) (>= (* x14 x4) 1))) (and (and (> ?v_9 0) (>= ?v_9 0)) (>= x8 1))) (and (and (and (> ?v_10 ?v_11) (>= ?v_10 ?v_11)) (>= x8 (* x14 x8))) (>= (* x9 x4) (* x14 x9)))) (and (> ?v_12 x15) (>= ?v_12 x15))) (and (and (and (> ?v_14 ?v_15) (>= ?v_14 ?v_15)) (>= (* x17 x4) (* x4 (* x17 x8)))) (>= ?v_16 (* x4 (+ (* x17 x9) ?v_16))))) ?v_17))))))
+(check-sat)
+(exit)
diff --git a/tests/regress/mcsat/nra/matrix-1-all-01.smt2.gold b/tests/regress/mcsat/nra/matrix-1-all-01.smt2.gold
new file mode 100644
index 000000000..6b8a2c3d2
--- /dev/null
+++ b/tests/regress/mcsat/nra/matrix-1-all-01.smt2.gold
@@ -0,0 +1 @@
+sat
diff --git a/tests/regress/mcsat/nra/mbo_E22E23.smt2 b/tests/regress/mcsat/nra/mbo_E22E23.smt2
new file mode 100644
index 000000000..ac48a5689
--- /dev/null
+++ b/tests/regress/mcsat/nra/mbo_E22E23.smt2
@@ -0,0 +1,47 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :author |Thomas Sturm, CNRS France, http://science.thomas-sturm.de|)
+(set-info :source |
+Transmitted by: Thomas Sturm
+Generated on: 20161105
+Received on: 20161105
+Generator: RedLog, http://www.redlog.eu/
+Application: qualitative analysis of systems of ODE in physics, chemistry, and the life sciences
+Publication: Algebraic Biology 2008, doi:10.1007/978-3-540-85101-1_15
+Additional information:
+All problems have the following form: a certain polynomial has a zero where all variables are positive.  Interval solutions for satisfiable problems is a valuable information.
+|)
+(set-info :series |MBO - Methylene Blue Oscillator System|)
+(set-info :instance |E22E23|)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-const j2 Real)
+(declare-const h6 Real)
+(declare-const h5 Real)
+(declare-const h4 Real)
+(declare-const h3 Real)
+(declare-const h1 Real)
+(assert (and (> h1 0) (> h3 0) (> h4 0) (> h5 0) (> h6 0) (> j2 0) (= (+ (* (* 
+h1 h1) h3 j2) (* (* h1 h1) h5 j2) (* (* h1 h1) h5) (* (* h1 h1) h6 j2) (* (* h1 
+h1) h6) (* h1 (* h3 h3) (* j2 j2)) (* h1 (* h3 h3) j2) (* 2 h1 h3 h4 j2) (* h1 
+h3 h4) (* 2 h1 h3 h5 (* j2 j2)) (* 4 h1 h3 h5 j2) (* 2 h1 h3 h5) (* 2 h1 h3 h6 
+(* j2 j2)) (* 5 h1 h3 h6 j2) (* 2 h1 h3 h6) (* 2 h1 h4 h5 j2) (* 2 h1 h4 h5) (* 
+2 h1 h4 h6 j2) (* h1 h4 h6) (* h1 (* h5 h5) (* j2 j2)) (* 2 h1 (* h5 h5) j2) (* 
+h1 (* h5 h5)) (* 2 h1 h5 h6 (* j2 j2)) (* 4 h1 h5 h6 j2) (* 2 h1 h5 h6) (* h1 
+(* h6 h6) (* j2 j2)) (* 2 h1 (* h6 h6) j2) (* h1 (* h6 h6)) (* (* h3 h3) h4 (* 
+j2 j2)) (* 2 (* h3 h3) h4 j2) (* (* h3 h3) h4) (* (* h3 h3) h5 (* j2 j2 j2)) (* 
+3 (* h3 h3) h5 (* j2 j2)) (* 3 (* h3 h3) h5 j2) (* (* h3 h3) h5) (* 2 (* h3 h3) 
+h6 (* j2 j2)) (* 3 (* h3 h3) h6 j2) (* (* h3 h3) h6) (* h3 (* h4 h4) j2) (* h3 
+(* h4 h4)) (* 2 h3 h4 h5 (* j2 j2)) (* 4 h3 h4 h5 j2) (* 2 h3 h4 h5) (* 2 h3 h4 
+h6 (* j2 j2)) (* 5 h3 h4 h6 j2) (* 2 h3 h4 h6) (* h3 (* h5 h5) (* j2 j2 j2)) (* 
+3 h3 (* h5 h5) (* j2 j2)) (* 3 h3 (* h5 h5) j2) (* h3 (* h5 h5)) (* 2 h3 h5 h6 
+(* j2 j2 j2)) (* 6 h3 h5 h6 (* j2 j2)) (* 6 h3 h5 h6 j2) (* 2 h3 h5 h6) (* 2 h3 
+(* h6 h6) (* j2 j2)) (* 3 h3 (* h6 h6) j2) (* h3 (* h6 h6)) (* (* h4 h4) h5 j2) 
+(* (* h4 h4) h5) (* (* h4 h4) h6 j2) (* h4 (* h5 h5) (* j2 j2)) (* 2 h4 (* h5 h5
+) j2) (* h4 (* h5 h5)) (* 2 h4 h5 h6 (* j2 j2)) (* 4 h4 h5 h6 j2) (* 2 h4 h5 h6)
+ (* h4 (* h6 h6) (* j2 j2)) (* h4 (* h6 h6) j2) (* (* h5 h5) h6 (* j2 j2 j2)) 
+(* 3 (* h5 h5) h6 (* j2 j2)) (* 3 (* h5 h5) h6 j2) (* (* h5 h5) h6) (* h5 (* h6 
+h6) (* j2 j2 j2)) (* 3 h5 (* h6 h6) (* j2 j2)) (* 3 h5 (* h6 h6) j2) (* h5 (* h6
+ h6))) 0)))
+(check-sat)
+(exit)
diff --git a/tests/regress/mcsat/nra/mbo_E22E23.smt2.gold b/tests/regress/mcsat/nra/mbo_E22E23.smt2.gold
new file mode 100644
index 000000000..3f65111b0
--- /dev/null
+++ b/tests/regress/mcsat/nra/mbo_E22E23.smt2.gold
@@ -0,0 +1 @@
+unsat
diff --git a/tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2 b/tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2
new file mode 100644
index 000000000..6d622f1e6
--- /dev/null
+++ b/tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2
@@ -0,0 +1,1304 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :source |Benchmarks generated from hycomp (https://es-static.fbk.eu/tools/hycomp/). BMC instances of non-linear hybrid automata taken from: Alessandro Cimatti, Sergio Mover, Stefano Tonetta, A quantifier-free SMT encoding of non-linear hybrid automata, FMCAD 2012 and Alessandro Cimatti, Sergio Mover, Stefano Tonetta, Quantier-free encoding of invariants for Hybrid Systems, Formal Methods in System Design. This instance solves a BMC problem of depth 2 and uses the quantifier free encoding with lemmas encoding. Contacts: Sergio Mover (mover@fbk.eu), Stefano Tonetta (tonettas@fbk.eu), Alessandro Cimatti (cimatti@fbk.eu).|)
+(set-info :category "industrial")
+(set-info :status unsat)
+;; MathSAT API call trace
+;; generated on Mon Mar 19 10:38:46 2012
+(declare-fun m.event_is_timed__AT0 () Bool)
+(declare-fun m.time__AT2 () Real)
+(declare-fun m.y__AT2 () Real)
+(declare-fun m.x__AT1 () Real)
+(declare-fun m.delta__AT2 () Real)
+(declare-fun m.x__AT2 () Real)
+(declare-fun m.EVENT.0__AT2 () Bool)
+(declare-fun m.EVENT.1__AT2 () Bool)
+(declare-fun m.delta__AT0 () Real)
+(declare-fun m.time__AT1 () Real)
+(declare-fun m.speed_y__AT0 () Real)
+(declare-fun m.EVENT.0__AT0 () Bool)
+(declare-fun m.delta__AT1 () Real)
+(declare-fun m.EVENT.1__AT0 () Bool)
+(declare-fun m.y__AT1 () Real)
+(declare-fun m.speed_x__AT2 () Real)
+(declare-fun m.speed_y__AT2 () Real)
+(declare-fun m.event_is_timed__AT1 () Bool)
+(declare-fun m.y__AT0 () Real)
+(declare-fun m.speed_x__AT1 () Real)
+(declare-fun m.speed_y__AT1 () Real)
+(declare-fun m.time__AT0 () Real)
+(declare-fun m.x__AT0 () Real)
+(declare-fun m.EVENT.0__AT1 () Bool)
+(declare-fun m.event_is_timed__AT2 () Bool)
+(declare-fun m.EVENT.1__AT1 () Bool)
+(declare-fun m.speed_x__AT0 () Real)
+(assert (let ((.def_1428 (* m.speed_y__AT2 m.delta__AT2)))
+(let ((.def_1429 (* 10.0 .def_1428)))
+(let ((.def_1101 (* m.delta__AT2 m.delta__AT2)))
+(let ((.def_1427 (* (- 49.0) .def_1101)))
+(let ((.def_1430 (+ .def_1427 .def_1429)))
+(let ((.def_1431 (* 10.0 m.y__AT2)))
+(let ((.def_1433 (+ .def_1431 .def_1430)))
+(let ((.def_1458 (<= .def_1433 0.0 )))
+(let ((.def_1466 (not .def_1458)))
+(let ((.def_1456 (<= m.y__AT2 0.0 )))
+(let ((.def_1467 (or .def_1456 .def_1466)))
+(let ((.def_1062 (<= 0.0 m.y__AT2)))
+(let ((.def_1464 (not .def_1062)))
+(let ((.def_1454 (<= 0.0 .def_1433)))
+(let ((.def_1465 (or .def_1454 .def_1464)))
+(let ((.def_1468 (and .def_1465 .def_1467)))
+(let ((.def_1269 (<= m.speed_y__AT2 0.0 )))
+(let ((.def_1270 (not .def_1269)))
+(let ((.def_1263 (* (- 49.0) m.delta__AT2)))
+(let ((.def_1264 (* 5.0 m.speed_y__AT2)))
+(let ((.def_1266 (+ .def_1264 .def_1263)))
+(let ((.def_1267 (<= .def_1266 0.0 )))
+(let ((.def_1268 (not .def_1267)))
+(let ((.def_1271 (or .def_1268 .def_1270)))
+(let ((.def_1272 (not .def_1271)))
+(let ((.def_1469 (or .def_1272 .def_1468)))
+(let ((.def_1460 (not .def_1454)))
+(let ((.def_1461 (or .def_1062 .def_1460)))
+(let ((.def_1457 (not .def_1456)))
+(let ((.def_1459 (or .def_1457 .def_1458)))
+(let ((.def_1462 (and .def_1459 .def_1461)))
+(let ((.def_1279 (<= 0.0 .def_1266)))
+(let ((.def_1280 (not .def_1279)))
+(let ((.def_1277 (<= 0.0 m.speed_y__AT2)))
+(let ((.def_1278 (not .def_1277)))
+(let ((.def_1281 (or .def_1278 .def_1280)))
+(let ((.def_1282 (not .def_1281)))
+(let ((.def_1463 (or .def_1282 .def_1462)))
+(let ((.def_1470 (and .def_1463 .def_1469)))
+(let ((.def_1455 (and .def_1062 .def_1454)))
+(let ((.def_1471 (and .def_1455 .def_1470)))
+(let ((.def_1291 (and .def_1267 .def_1269)))
+(let ((.def_1288 (or .def_1277 .def_1280)))
+(let ((.def_1287 (or .def_1267 .def_1270)))
+(let ((.def_1289 (and .def_1287 .def_1288)))
+(let ((.def_1292 (and .def_1289 .def_1291)))
+(let ((.def_1286 (and .def_1277 .def_1279)))
+(let ((.def_1290 (and .def_1286 .def_1289)))
+(let ((.def_1293 (or .def_1290 .def_1292)))
+(let ((.def_1472 (and .def_1293 .def_1471)))
+(let ((.def_1434 (<= .def_1433 1000.0 )))
+(let ((.def_1446 (not .def_1434)))
+(let ((.def_1061 (<= m.y__AT2 100.0 )))
+(let ((.def_1447 (or .def_1061 .def_1446)))
+(let ((.def_1440 (<= 100.0 m.y__AT2)))
+(let ((.def_1444 (not .def_1440)))
+(let ((.def_1438 (<= 1000.0 .def_1433)))
+(let ((.def_1445 (or .def_1438 .def_1444)))
+(let ((.def_1448 (and .def_1445 .def_1447)))
+(let ((.def_1449 (or .def_1272 .def_1448)))
+(let ((.def_1439 (not .def_1438)))
+(let ((.def_1441 (or .def_1439 .def_1440)))
+(let ((.def_1436 (not .def_1061)))
+(let ((.def_1437 (or .def_1434 .def_1436)))
+(let ((.def_1442 (and .def_1437 .def_1441)))
+(let ((.def_1443 (or .def_1282 .def_1442)))
+(let ((.def_1450 (and .def_1443 .def_1449)))
+(let ((.def_1435 (and .def_1061 .def_1434)))
+(let ((.def_1451 (and .def_1435 .def_1450)))
+(let ((.def_1452 (and .def_1293 .def_1451)))
+(let ((.def_1105 (* (- (/ 49 10)) m.speed_y__AT2)))
+(let ((.def_1151 (* 3.0 .def_1105)))
+(let ((.def_1324 (* (- 1.0) .def_1151)))
+(let ((.def_1352 (* 2.0 .def_1324)))
+(let ((.def_1396 (* (- 1.0) .def_1352)))
+(let ((.def_1397 (* m.delta__AT2 .def_1396)))
+(let ((.def_1398 (* (- 50.0) .def_1397)))
+(let ((.def_1121 (* m.speed_x__AT2 m.speed_x__AT2)))
+(let ((.def_1221 (* (- 50.0) .def_1121)))
+(let ((.def_1403 (+ .def_1221 .def_1398)))
+(let ((.def_1109 (* m.speed_y__AT2 m.speed_y__AT2)))
+(let ((.def_1219 (* (- 50.0) .def_1109)))
+(let ((.def_1404 (+ .def_1219 .def_1403)))
+(let ((.def_1223 (* (- 7203.0) .def_1101)))
+(let ((.def_1405 (+ .def_1223 .def_1404)))
+(let ((.def_1225 (* 490.0 m.y__AT2)))
+(let ((.def_1406 (+ .def_1225 .def_1405)))
+(let ((.def_1409 (<= 0.0 .def_1406)))
+(let ((.def_1416 (not .def_1409)))
+(let ((.def_1234 (* (- 5.0) .def_1121)))
+(let ((.def_1233 (* (- 5.0) .def_1109)))
+(let ((.def_1235 (+ .def_1233 .def_1234)))
+(let ((.def_1236 (* 49.0 m.y__AT2)))
+(let ((.def_1238 (+ .def_1236 .def_1235)))
+(let ((.def_1249 (<= 0.0 .def_1238)))
+(let ((.def_1417 (or .def_1249 .def_1416)))
+(let ((.def_1407 (<= .def_1406 0.0 )))
+(let ((.def_1239 (<= .def_1238 0.0 )))
+(let ((.def_1240 (not .def_1239)))
+(let ((.def_1415 (or .def_1240 .def_1407)))
+(let ((.def_1418 (and .def_1415 .def_1417)))
+(let ((.def_1419 (or .def_1282 .def_1418)))
+(let ((.def_1411 (not .def_1407)))
+(let ((.def_1412 (or .def_1239 .def_1411)))
+(let ((.def_1250 (not .def_1249)))
+(let ((.def_1410 (or .def_1250 .def_1409)))
+(let ((.def_1413 (and .def_1410 .def_1412)))
+(let ((.def_1414 (or .def_1272 .def_1413)))
+(let ((.def_1420 (and .def_1414 .def_1419)))
+(let ((.def_1408 (and .def_1239 .def_1407)))
+(let ((.def_1421 (and .def_1408 .def_1420)))
+(let ((.def_1422 (and .def_1293 .def_1421)))
+(let ((.def_1353 (* m.delta__AT2 .def_1352)))
+(let ((.def_1354 (* 50.0 .def_1353)))
+(let ((.def_1359 (+ .def_1221 .def_1354)))
+(let ((.def_1360 (+ .def_1219 .def_1359)))
+(let ((.def_1361 (+ .def_1223 .def_1360)))
+(let ((.def_1362 (+ .def_1225 .def_1361)))
+(let ((.def_1373 (<= .def_1362 0.0 )))
+(let ((.def_1374 (not .def_1373)))
+(let ((.def_1390 (or .def_1239 .def_1374)))
+(let ((.def_1363 (<= 0.0 .def_1362)))
+(let ((.def_1389 (or .def_1250 .def_1363)))
+(let ((.def_1391 (and .def_1389 .def_1390)))
+(let ((.def_1392 (or .def_1272 .def_1391)))
+(let ((.def_1364 (not .def_1363)))
+(let ((.def_1386 (or .def_1249 .def_1364)))
+(let ((.def_1385 (or .def_1240 .def_1373)))
+(let ((.def_1387 (and .def_1385 .def_1386)))
+(let ((.def_1388 (or .def_1282 .def_1387)))
+(let ((.def_1393 (and .def_1388 .def_1392)))
+(let ((.def_1384 (and .def_1249 .def_1363)))
+(let ((.def_1394 (and .def_1384 .def_1393)))
+(let ((.def_1395 (and .def_1293 .def_1394)))
+(let ((.def_1423 (or .def_1395 .def_1422)))
+(let ((.def_1162 (* 2.0 .def_1121)))
+(let ((.def_1336 (* (- 1.0) .def_1162)))
+(let ((.def_1337 (* m.delta__AT2 .def_1336)))
+(let ((.def_1338 (* 25.0 .def_1337)))
+(let ((.def_1113 (* (- (/ 49 10)) m.y__AT2)))
+(let ((.def_1158 (* 2.0 .def_1113)))
+(let ((.def_1332 (* (- 1.0) .def_1158)))
+(let ((.def_1333 (* m.delta__AT2 .def_1332)))
+(let ((.def_1334 (* 50.0 .def_1333)))
+(let ((.def_1343 (+ .def_1334 .def_1338)))
+(let ((.def_1154 (* 2.0 .def_1109)))
+(let ((.def_1328 (* (- 1.0) .def_1154)))
+(let ((.def_1329 (* m.delta__AT2 .def_1328)))
+(let ((.def_1330 (* 25.0 .def_1329)))
+(let ((.def_1344 (+ .def_1330 .def_1343)))
+(let ((.def_1325 (* .def_1101 .def_1324)))
+(let ((.def_1326 (* 50.0 .def_1325)))
+(let ((.def_1345 (+ .def_1326 .def_1344)))
+(let ((.def_1125 (* m.x__AT2 m.speed_x__AT2)))
+(let ((.def_1170 (* (- 50.0) .def_1125)))
+(let ((.def_1346 (+ .def_1170 .def_1345)))
+(let ((.def_1117 (* m.y__AT2 m.speed_y__AT2)))
+(let ((.def_1168 (* (- 50.0) .def_1117)))
+(let ((.def_1347 (+ .def_1168 .def_1346)))
+(let ((.def_1102 (* m.delta__AT2 .def_1101)))
+(let ((.def_1166 (* (- 2401.0) .def_1102)))
+(let ((.def_1348 (+ .def_1166 .def_1347)))
+(let ((.def_1172 (* 1000.0 m.speed_x__AT2)))
+(let ((.def_1349 (+ .def_1172 .def_1348)))
+(let ((.def_1367 (<= .def_1349 0.0 )))
+(let ((.def_1378 (not .def_1367)))
+(let ((.def_1184 (* (- 1.0) .def_1125)))
+(let ((.def_1183 (* (- 1.0) .def_1117)))
+(let ((.def_1185 (+ .def_1183 .def_1184)))
+(let ((.def_1186 (* 20.0 m.speed_x__AT2)))
+(let ((.def_1188 (+ .def_1186 .def_1185)))
+(let ((.def_1189 (<= .def_1188 0.0 )))
+(let ((.def_1379 (or .def_1189 .def_1378)))
+(let ((.def_1350 (<= 0.0 .def_1349)))
+(let ((.def_1203 (<= 0.0 .def_1188)))
+(let ((.def_1204 (not .def_1203)))
+(let ((.def_1377 (or .def_1204 .def_1350)))
+(let ((.def_1380 (and .def_1377 .def_1379)))
+(let ((.def_1375 (or .def_1240 .def_1374)))
+(let ((.def_1376 (not .def_1375)))
+(let ((.def_1381 (or .def_1376 .def_1380)))
+(let ((.def_1369 (not .def_1350)))
+(let ((.def_1370 (or .def_1203 .def_1369)))
+(let ((.def_1190 (not .def_1189)))
+(let ((.def_1368 (or .def_1190 .def_1367)))
+(let ((.def_1371 (and .def_1368 .def_1370)))
+(let ((.def_1365 (or .def_1250 .def_1364)))
+(let ((.def_1366 (not .def_1365)))
+(let ((.def_1372 (or .def_1366 .def_1371)))
+(let ((.def_1382 (and .def_1372 .def_1381)))
+(let ((.def_1351 (and .def_1203 .def_1350)))
+(let ((.def_1383 (and .def_1351 .def_1382)))
+(let ((.def_1424 (and .def_1383 .def_1423)))
+(let ((.def_1216 (* 2.0 .def_1151)))
+(let ((.def_1295 (* (- 1.0) .def_1216)))
+(let ((.def_1296 (* m.delta__AT2 .def_1295)))
+(let ((.def_1297 (* 50.0 .def_1296)))
+(let ((.def_1302 (+ .def_1221 .def_1297)))
+(let ((.def_1303 (+ .def_1219 .def_1302)))
+(let ((.def_1304 (+ .def_1223 .def_1303)))
+(let ((.def_1305 (+ .def_1225 .def_1304)))
+(let ((.def_1308 (<= .def_1305 0.0 )))
+(let ((.def_1315 (not .def_1308)))
+(let ((.def_1316 (or .def_1239 .def_1315)))
+(let ((.def_1306 (<= 0.0 .def_1305)))
+(let ((.def_1314 (or .def_1250 .def_1306)))
+(let ((.def_1317 (and .def_1314 .def_1316)))
+(let ((.def_1318 (or .def_1272 .def_1317)))
+(let ((.def_1310 (not .def_1306)))
+(let ((.def_1311 (or .def_1249 .def_1310)))
+(let ((.def_1309 (or .def_1240 .def_1308)))
+(let ((.def_1312 (and .def_1309 .def_1311)))
+(let ((.def_1313 (or .def_1282 .def_1312)))
+(let ((.def_1319 (and .def_1313 .def_1318)))
+(let ((.def_1307 (and .def_1249 .def_1306)))
+(let ((.def_1320 (and .def_1307 .def_1319)))
+(let ((.def_1321 (and .def_1293 .def_1320)))
+(let ((.def_1217 (* m.delta__AT2 .def_1216)))
+(let ((.def_1218 (* (- 50.0) .def_1217)))
+(let ((.def_1227 (+ .def_1221 .def_1218)))
+(let ((.def_1228 (+ .def_1219 .def_1227)))
+(let ((.def_1229 (+ .def_1223 .def_1228)))
+(let ((.def_1230 (+ .def_1225 .def_1229)))
+(let ((.def_1247 (<= 0.0 .def_1230)))
+(let ((.def_1248 (not .def_1247)))
+(let ((.def_1275 (or .def_1248 .def_1249)))
+(let ((.def_1231 (<= .def_1230 0.0 )))
+(let ((.def_1274 (or .def_1231 .def_1240)))
+(let ((.def_1276 (and .def_1274 .def_1275)))
+(let ((.def_1283 (or .def_1276 .def_1282)))
+(let ((.def_1232 (not .def_1231)))
+(let ((.def_1261 (or .def_1232 .def_1239)))
+(let ((.def_1260 (or .def_1247 .def_1250)))
+(let ((.def_1262 (and .def_1260 .def_1261)))
+(let ((.def_1273 (or .def_1262 .def_1272)))
+(let ((.def_1284 (and .def_1273 .def_1283)))
+(let ((.def_1259 (and .def_1231 .def_1239)))
+(let ((.def_1285 (and .def_1259 .def_1284)))
+(let ((.def_1294 (and .def_1285 .def_1293)))
+(let ((.def_1322 (or .def_1294 .def_1321)))
+(let ((.def_1163 (* m.delta__AT2 .def_1162)))
+(let ((.def_1164 (* (- 25.0) .def_1163)))
+(let ((.def_1159 (* m.delta__AT2 .def_1158)))
+(let ((.def_1160 (* (- 50.0) .def_1159)))
+(let ((.def_1174 (+ .def_1160 .def_1164)))
+(let ((.def_1155 (* m.delta__AT2 .def_1154)))
+(let ((.def_1156 (* (- 25.0) .def_1155)))
+(let ((.def_1175 (+ .def_1156 .def_1174)))
+(let ((.def_1152 (* .def_1101 .def_1151)))
+(let ((.def_1153 (* (- 50.0) .def_1152)))
+(let ((.def_1176 (+ .def_1153 .def_1175)))
+(let ((.def_1177 (+ .def_1170 .def_1176)))
+(let ((.def_1178 (+ .def_1168 .def_1177)))
+(let ((.def_1179 (+ .def_1166 .def_1178)))
+(let ((.def_1180 (+ .def_1172 .def_1179)))
+(let ((.def_1201 (<= 0.0 .def_1180)))
+(let ((.def_1202 (not .def_1201)))
+(let ((.def_1254 (or .def_1202 .def_1203)))
+(let ((.def_1181 (<= .def_1180 0.0 )))
+(let ((.def_1253 (or .def_1181 .def_1190)))
+(let ((.def_1255 (and .def_1253 .def_1254)))
+(let ((.def_1251 (or .def_1248 .def_1250)))
+(let ((.def_1252 (not .def_1251)))
+(let ((.def_1256 (or .def_1252 .def_1255)))
+(let ((.def_1182 (not .def_1181)))
+(let ((.def_1244 (or .def_1182 .def_1189)))
+(let ((.def_1243 (or .def_1201 .def_1204)))
+(let ((.def_1245 (and .def_1243 .def_1244)))
+(let ((.def_1241 (or .def_1232 .def_1240)))
+(let ((.def_1242 (not .def_1241)))
+(let ((.def_1246 (or .def_1242 .def_1245)))
+(let ((.def_1257 (and .def_1246 .def_1256)))
+(let ((.def_1215 (and .def_1181 .def_1189)))
+(let ((.def_1258 (and .def_1215 .def_1257)))
+(let ((.def_1323 (and .def_1258 .def_1322)))
+(let ((.def_1425 (or .def_1323 .def_1424)))
+(let ((.def_1129 (* (- 20.0) m.speed_x__AT2)))
+(let ((.def_1130 (* m.delta__AT2 .def_1129)))
+(let ((.def_1131 (* (- 200.0) .def_1130)))
+(let ((.def_1126 (* m.delta__AT2 .def_1125)))
+(let ((.def_1127 (* (- 200.0) .def_1126)))
+(let ((.def_1139 (+ .def_1127 .def_1131)))
+(let ((.def_1122 (* .def_1101 .def_1121)))
+(let ((.def_1123 (* (- 100.0) .def_1122)))
+(let ((.def_1140 (+ .def_1123 .def_1139)))
+(let ((.def_1118 (* m.delta__AT2 .def_1117)))
+(let ((.def_1119 (* (- 200.0) .def_1118)))
+(let ((.def_1141 (+ .def_1119 .def_1140)))
+(let ((.def_1114 (* .def_1101 .def_1113)))
+(let ((.def_1115 (* (- 200.0) .def_1114)))
+(let ((.def_1142 (+ .def_1115 .def_1141)))
+(let ((.def_1110 (* .def_1101 .def_1109)))
+(let ((.def_1111 (* (- 100.0) .def_1110)))
+(let ((.def_1143 (+ .def_1111 .def_1142)))
+(let ((.def_1106 (* .def_1102 .def_1105)))
+(let ((.def_1107 (* (- 200.0) .def_1106)))
+(let ((.def_1144 (+ .def_1107 .def_1143)))
+(let ((.def_1103 (* m.delta__AT2 .def_1102)))
+(let ((.def_1104 (* (- 2401.0) .def_1103)))
+(let ((.def_1145 (+ .def_1104 .def_1144)))
+(let ((.def_1094 (* m.x__AT2 m.x__AT2)))
+(let ((.def_1135 (* (- 100.0) .def_1094)))
+(let ((.def_1146 (+ .def_1135 .def_1145)))
+(let ((.def_1056 (* m.y__AT2 m.y__AT2)))
+(let ((.def_1133 (* (- 100.0) .def_1056)))
+(let ((.def_1147 (+ .def_1133 .def_1146)))
+(let ((.def_1137 (* 4000.0 m.x__AT2)))
+(let ((.def_1148 (+ .def_1137 .def_1147)))
+(let ((.def_1195 (<= 0.0 .def_1148)))
+(let ((.def_1209 (not .def_1195)))
+(let ((.def_1095 (* (- 1.0) .def_1094)))
+(let ((.def_1093 (* (- 1.0) .def_1056)))
+(let ((.def_1096 (+ .def_1093 .def_1095)))
+(let ((.def_1097 (* 40.0 m.x__AT2)))
+(let ((.def_1099 (+ .def_1097 .def_1096)))
+(let ((.def_1193 (<= 0.0 .def_1099)))
+(let ((.def_1210 (or .def_1193 .def_1209)))
+(let ((.def_1100 (<= .def_1099 0.0 )))
+(let ((.def_1207 (not .def_1100)))
+(let ((.def_1149 (<= .def_1148 0.0 )))
+(let ((.def_1208 (or .def_1149 .def_1207)))
+(let ((.def_1211 (and .def_1208 .def_1210)))
+(let ((.def_1205 (or .def_1202 .def_1204)))
+(let ((.def_1206 (not .def_1205)))
+(let ((.def_1212 (or .def_1206 .def_1211)))
+(let ((.def_1197 (not .def_1149)))
+(let ((.def_1198 (or .def_1100 .def_1197)))
+(let ((.def_1194 (not .def_1193)))
+(let ((.def_1196 (or .def_1194 .def_1195)))
+(let ((.def_1199 (and .def_1196 .def_1198)))
+(let ((.def_1191 (or .def_1182 .def_1190)))
+(let ((.def_1192 (not .def_1191)))
+(let ((.def_1200 (or .def_1192 .def_1199)))
+(let ((.def_1213 (and .def_1200 .def_1212)))
+(let ((.def_1150 (and .def_1100 .def_1149)))
+(let ((.def_1214 (and .def_1150 .def_1213)))
+(let ((.def_1426 (and .def_1214 .def_1425)))
+(let ((.def_1453 (and .def_1426 .def_1452)))
+(let ((.def_1473 (and .def_1453 .def_1472)))
+(let ((.def_1071 (* m.speed_x__AT2 m.delta__AT2)))
+(let ((.def_1072 (+ m.x__AT2 .def_1071)))
+(let ((.def_1078 (<= .def_1072 0.0 )))
+(let ((.def_1087 (not .def_1078)))
+(let ((.def_1076 (<= m.x__AT2 0.0 )))
+(let ((.def_1088 (or .def_1076 .def_1087)))
+(let ((.def_1059 (<= 0.0 m.x__AT2)))
+(let ((.def_1085 (not .def_1059)))
+(let ((.def_1073 (<= 0.0 .def_1072)))
+(let ((.def_1086 (or .def_1073 .def_1085)))
+(let ((.def_1089 (and .def_1086 .def_1088)))
+(let ((.def_1084 (<= m.speed_x__AT2 0.0 )))
+(let ((.def_1090 (or .def_1084 .def_1089)))
+(let ((.def_1080 (not .def_1073)))
+(let ((.def_1081 (or .def_1059 .def_1080)))
+(let ((.def_1077 (not .def_1076)))
+(let ((.def_1079 (or .def_1077 .def_1078)))
+(let ((.def_1082 (and .def_1079 .def_1081)))
+(let ((.def_1075 (<= 0.0 m.speed_x__AT2)))
+(let ((.def_1083 (or .def_1075 .def_1082)))
+(let ((.def_1091 (and .def_1083 .def_1090)))
+(let ((.def_1074 (and .def_1059 .def_1073)))
+(let ((.def_1092 (and .def_1074 .def_1091)))
+(let ((.def_1474 (and .def_1092 .def_1473)))
+(let ((.def_1067 (<= m.x__AT1 20.0 )))
+(let ((.def_1063 (and .def_1061 .def_1062)))
+(let ((.def_1054 (+ m.x__AT2 (- 20.0) )))
+(let ((.def_1055 (* .def_1054 .def_1054)))
+(let ((.def_1057 (+ .def_1055 .def_1056)))
+(let ((.def_1058 (<= 400.0 .def_1057)))
+(let ((.def_1060 (and .def_1058 .def_1059)))
+(let ((.def_1064 (and .def_1060 .def_1063)))
+(let ((.def_1052 (not m.EVENT.0__AT2)))
+(let ((.def_1050 (not m.EVENT.1__AT2)))
+(let ((.def_1053 (or .def_1050 .def_1052)))
+(let ((.def_1065 (and .def_1053 .def_1064)))
+(let ((.def_1044 (<= 0.0 m.delta__AT1)))
+(let ((.def_551 (not m.EVENT.0__AT1)))
+(let ((.def_549 (not m.EVENT.1__AT1)))
+(let ((.def_975 (and .def_549 .def_551)))
+(let ((.def_977 (not .def_975)))
+(let ((.def_1045 (or .def_977 .def_1044)))
+(let ((.def_1046 (or m.EVENT.1__AT1 .def_1045)))
+(let ((.def_1032 (* (- 10.0) m.y__AT2)))
+(let ((.def_927 (* m.speed_y__AT1 m.delta__AT1)))
+(let ((.def_928 (* 10.0 .def_927)))
+(let ((.def_1036 (+ .def_928 .def_1032)))
+(let ((.def_600 (* m.delta__AT1 m.delta__AT1)))
+(let ((.def_926 (* (- 49.0) .def_600)))
+(let ((.def_1037 (+ .def_926 .def_1036)))
+(let ((.def_930 (* 10.0 m.y__AT1)))
+(let ((.def_1038 (+ .def_930 .def_1037)))
+(let ((.def_1039 (= .def_1038 0.0 )))
+(let ((.def_1027 (* (- 5.0) m.speed_y__AT2)))
+(let ((.def_762 (* (- 49.0) m.delta__AT1)))
+(let ((.def_1028 (+ .def_762 .def_1027)))
+(let ((.def_763 (* 5.0 m.speed_y__AT1)))
+(let ((.def_1029 (+ .def_763 .def_1028)))
+(let ((.def_1030 (= .def_1029 0.0 )))
+(let ((.def_570 (* m.speed_x__AT1 m.delta__AT1)))
+(let ((.def_1022 (* (- 1.0) .def_570)))
+(let ((.def_521 (* (- 1.0) m.x__AT1)))
+(let ((.def_1023 (+ .def_521 .def_1022)))
+(let ((.def_1024 (+ m.x__AT2 .def_1023)))
+(let ((.def_1025 (= .def_1024 0.0 )))
+(let ((.def_1000 (= m.speed_x__AT1 m.speed_x__AT2)))
+(let ((.def_1026 (and .def_1000 .def_1025)))
+(let ((.def_1031 (and .def_1026 .def_1030)))
+(let ((.def_1040 (and .def_1031 .def_1039)))
+(let ((.def_1041 (or .def_977 .def_1040)))
+(let ((.def_1013 (= m.delta__AT1 0.0 )))
+(let ((.def_1014 (and .def_975 .def_1013)))
+(let ((.def_1015 (not .def_1014)))
+(let ((.def_997 (= m.y__AT1 m.y__AT2)))
+(let ((.def_994 (= m.x__AT2 m.x__AT1)))
+(let ((.def_1008 (and .def_994 .def_997)))
+(let ((.def_1009 (and .def_1000 .def_1008)))
+(let ((.def_1003 (= m.speed_y__AT1 m.speed_y__AT2)))
+(let ((.def_1010 (and .def_1003 .def_1009)))
+(let ((.def_1016 (or .def_1010 .def_1015)))
+(let ((.def_1017 (or m.EVENT.1__AT1 .def_1016)))
+(let ((.def_1011 (or .def_975 .def_1010)))
+(let ((.def_1012 (or m.EVENT.1__AT1 .def_1011)))
+(let ((.def_1018 (and .def_1012 .def_1017)))
+(let ((.def_1042 (and .def_1018 .def_1041)))
+(let ((.def_982 (= m.time__AT1 m.time__AT2)))
+(let ((.def_995 (and .def_982 .def_994)))
+(let ((.def_998 (and .def_995 .def_997)))
+(let ((.def_1001 (and .def_998 .def_1000)))
+(let ((.def_1004 (and .def_1001 .def_1003)))
+(let ((.def_1005 (or .def_549 .def_1004)))
+(let ((.def_985 (* (- 1.0) m.time__AT2)))
+(let ((.def_988 (+ m.delta__AT1 .def_985)))
+(let ((.def_989 (+ m.time__AT1 .def_988)))
+(let ((.def_990 (= .def_989 0.0 )))
+(let ((.def_991 (or .def_977 .def_990)))
+(let ((.def_992 (or m.EVENT.1__AT1 .def_991)))
+(let ((.def_983 (or .def_975 .def_982)))
+(let ((.def_984 (or m.EVENT.1__AT1 .def_983)))
+(let ((.def_993 (and .def_984 .def_992)))
+(let ((.def_1006 (and .def_993 .def_1005)))
+(let ((.def_979 (= .def_977 m.event_is_timed__AT2)))
+(let ((.def_976 (= m.event_is_timed__AT1 .def_975)))
+(let ((.def_980 (and .def_976 .def_979)))
+(let ((.def_1007 (and .def_980 .def_1006)))
+(let ((.def_1043 (and .def_1007 .def_1042)))
+(let ((.def_1047 (and .def_1043 .def_1046)))
+(let ((.def_1048 (and .def_549 .def_1047)))
+(let ((.def_1066 (and .def_1048 .def_1065)))
+(let ((.def_1068 (and .def_1066 .def_1067)))
+(let ((.def_929 (+ .def_926 .def_928)))
+(let ((.def_932 (+ .def_930 .def_929)))
+(let ((.def_957 (<= .def_932 0.0 )))
+(let ((.def_965 (not .def_957)))
+(let ((.def_955 (<= m.y__AT1 0.0 )))
+(let ((.def_966 (or .def_955 .def_965)))
+(let ((.def_561 (<= 0.0 m.y__AT1)))
+(let ((.def_963 (not .def_561)))
+(let ((.def_953 (<= 0.0 .def_932)))
+(let ((.def_964 (or .def_953 .def_963)))
+(let ((.def_967 (and .def_964 .def_966)))
+(let ((.def_768 (<= m.speed_y__AT1 0.0 )))
+(let ((.def_769 (not .def_768)))
+(let ((.def_765 (+ .def_763 .def_762)))
+(let ((.def_766 (<= .def_765 0.0 )))
+(let ((.def_767 (not .def_766)))
+(let ((.def_770 (or .def_767 .def_769)))
+(let ((.def_771 (not .def_770)))
+(let ((.def_968 (or .def_771 .def_967)))
+(let ((.def_959 (not .def_953)))
+(let ((.def_960 (or .def_561 .def_959)))
+(let ((.def_956 (not .def_955)))
+(let ((.def_958 (or .def_956 .def_957)))
+(let ((.def_961 (and .def_958 .def_960)))
+(let ((.def_778 (<= 0.0 .def_765)))
+(let ((.def_779 (not .def_778)))
+(let ((.def_776 (<= 0.0 m.speed_y__AT1)))
+(let ((.def_777 (not .def_776)))
+(let ((.def_780 (or .def_777 .def_779)))
+(let ((.def_781 (not .def_780)))
+(let ((.def_962 (or .def_781 .def_961)))
+(let ((.def_969 (and .def_962 .def_968)))
+(let ((.def_954 (and .def_561 .def_953)))
+(let ((.def_970 (and .def_954 .def_969)))
+(let ((.def_790 (and .def_766 .def_768)))
+(let ((.def_787 (or .def_776 .def_779)))
+(let ((.def_786 (or .def_766 .def_769)))
+(let ((.def_788 (and .def_786 .def_787)))
+(let ((.def_791 (and .def_788 .def_790)))
+(let ((.def_785 (and .def_776 .def_778)))
+(let ((.def_789 (and .def_785 .def_788)))
+(let ((.def_792 (or .def_789 .def_791)))
+(let ((.def_971 (and .def_792 .def_970)))
+(let ((.def_933 (<= .def_932 1000.0 )))
+(let ((.def_945 (not .def_933)))
+(let ((.def_560 (<= m.y__AT1 100.0 )))
+(let ((.def_946 (or .def_560 .def_945)))
+(let ((.def_939 (<= 100.0 m.y__AT1)))
+(let ((.def_943 (not .def_939)))
+(let ((.def_937 (<= 1000.0 .def_932)))
+(let ((.def_944 (or .def_937 .def_943)))
+(let ((.def_947 (and .def_944 .def_946)))
+(let ((.def_948 (or .def_771 .def_947)))
+(let ((.def_938 (not .def_937)))
+(let ((.def_940 (or .def_938 .def_939)))
+(let ((.def_935 (not .def_560)))
+(let ((.def_936 (or .def_933 .def_935)))
+(let ((.def_941 (and .def_936 .def_940)))
+(let ((.def_942 (or .def_781 .def_941)))
+(let ((.def_949 (and .def_942 .def_948)))
+(let ((.def_934 (and .def_560 .def_933)))
+(let ((.def_950 (and .def_934 .def_949)))
+(let ((.def_951 (and .def_792 .def_950)))
+(let ((.def_604 (* (- (/ 49 10)) m.speed_y__AT1)))
+(let ((.def_650 (* 3.0 .def_604)))
+(let ((.def_823 (* (- 1.0) .def_650)))
+(let ((.def_851 (* 2.0 .def_823)))
+(let ((.def_895 (* (- 1.0) .def_851)))
+(let ((.def_896 (* m.delta__AT1 .def_895)))
+(let ((.def_897 (* (- 50.0) .def_896)))
+(let ((.def_620 (* m.speed_x__AT1 m.speed_x__AT1)))
+(let ((.def_720 (* (- 50.0) .def_620)))
+(let ((.def_902 (+ .def_720 .def_897)))
+(let ((.def_608 (* m.speed_y__AT1 m.speed_y__AT1)))
+(let ((.def_718 (* (- 50.0) .def_608)))
+(let ((.def_903 (+ .def_718 .def_902)))
+(let ((.def_722 (* (- 7203.0) .def_600)))
+(let ((.def_904 (+ .def_722 .def_903)))
+(let ((.def_724 (* 490.0 m.y__AT1)))
+(let ((.def_905 (+ .def_724 .def_904)))
+(let ((.def_908 (<= 0.0 .def_905)))
+(let ((.def_915 (not .def_908)))
+(let ((.def_733 (* (- 5.0) .def_620)))
+(let ((.def_732 (* (- 5.0) .def_608)))
+(let ((.def_734 (+ .def_732 .def_733)))
+(let ((.def_735 (* 49.0 m.y__AT1)))
+(let ((.def_737 (+ .def_735 .def_734)))
+(let ((.def_748 (<= 0.0 .def_737)))
+(let ((.def_916 (or .def_748 .def_915)))
+(let ((.def_906 (<= .def_905 0.0 )))
+(let ((.def_738 (<= .def_737 0.0 )))
+(let ((.def_739 (not .def_738)))
+(let ((.def_914 (or .def_739 .def_906)))
+(let ((.def_917 (and .def_914 .def_916)))
+(let ((.def_918 (or .def_781 .def_917)))
+(let ((.def_910 (not .def_906)))
+(let ((.def_911 (or .def_738 .def_910)))
+(let ((.def_749 (not .def_748)))
+(let ((.def_909 (or .def_749 .def_908)))
+(let ((.def_912 (and .def_909 .def_911)))
+(let ((.def_913 (or .def_771 .def_912)))
+(let ((.def_919 (and .def_913 .def_918)))
+(let ((.def_907 (and .def_738 .def_906)))
+(let ((.def_920 (and .def_907 .def_919)))
+(let ((.def_921 (and .def_792 .def_920)))
+(let ((.def_852 (* m.delta__AT1 .def_851)))
+(let ((.def_853 (* 50.0 .def_852)))
+(let ((.def_858 (+ .def_720 .def_853)))
+(let ((.def_859 (+ .def_718 .def_858)))
+(let ((.def_860 (+ .def_722 .def_859)))
+(let ((.def_861 (+ .def_724 .def_860)))
+(let ((.def_872 (<= .def_861 0.0 )))
+(let ((.def_873 (not .def_872)))
+(let ((.def_889 (or .def_738 .def_873)))
+(let ((.def_862 (<= 0.0 .def_861)))
+(let ((.def_888 (or .def_749 .def_862)))
+(let ((.def_890 (and .def_888 .def_889)))
+(let ((.def_891 (or .def_771 .def_890)))
+(let ((.def_863 (not .def_862)))
+(let ((.def_885 (or .def_748 .def_863)))
+(let ((.def_884 (or .def_739 .def_872)))
+(let ((.def_886 (and .def_884 .def_885)))
+(let ((.def_887 (or .def_781 .def_886)))
+(let ((.def_892 (and .def_887 .def_891)))
+(let ((.def_883 (and .def_748 .def_862)))
+(let ((.def_893 (and .def_883 .def_892)))
+(let ((.def_894 (and .def_792 .def_893)))
+(let ((.def_922 (or .def_894 .def_921)))
+(let ((.def_661 (* 2.0 .def_620)))
+(let ((.def_835 (* (- 1.0) .def_661)))
+(let ((.def_836 (* m.delta__AT1 .def_835)))
+(let ((.def_837 (* 25.0 .def_836)))
+(let ((.def_612 (* (- (/ 49 10)) m.y__AT1)))
+(let ((.def_657 (* 2.0 .def_612)))
+(let ((.def_831 (* (- 1.0) .def_657)))
+(let ((.def_832 (* m.delta__AT1 .def_831)))
+(let ((.def_833 (* 50.0 .def_832)))
+(let ((.def_842 (+ .def_833 .def_837)))
+(let ((.def_653 (* 2.0 .def_608)))
+(let ((.def_827 (* (- 1.0) .def_653)))
+(let ((.def_828 (* m.delta__AT1 .def_827)))
+(let ((.def_829 (* 25.0 .def_828)))
+(let ((.def_843 (+ .def_829 .def_842)))
+(let ((.def_824 (* .def_600 .def_823)))
+(let ((.def_825 (* 50.0 .def_824)))
+(let ((.def_844 (+ .def_825 .def_843)))
+(let ((.def_624 (* m.x__AT1 m.speed_x__AT1)))
+(let ((.def_669 (* (- 50.0) .def_624)))
+(let ((.def_845 (+ .def_669 .def_844)))
+(let ((.def_616 (* m.y__AT1 m.speed_y__AT1)))
+(let ((.def_667 (* (- 50.0) .def_616)))
+(let ((.def_846 (+ .def_667 .def_845)))
+(let ((.def_601 (* m.delta__AT1 .def_600)))
+(let ((.def_665 (* (- 2401.0) .def_601)))
+(let ((.def_847 (+ .def_665 .def_846)))
+(let ((.def_671 (* 1000.0 m.speed_x__AT1)))
+(let ((.def_848 (+ .def_671 .def_847)))
+(let ((.def_866 (<= .def_848 0.0 )))
+(let ((.def_877 (not .def_866)))
+(let ((.def_683 (* (- 1.0) .def_624)))
+(let ((.def_682 (* (- 1.0) .def_616)))
+(let ((.def_684 (+ .def_682 .def_683)))
+(let ((.def_685 (* 20.0 m.speed_x__AT1)))
+(let ((.def_687 (+ .def_685 .def_684)))
+(let ((.def_688 (<= .def_687 0.0 )))
+(let ((.def_878 (or .def_688 .def_877)))
+(let ((.def_849 (<= 0.0 .def_848)))
+(let ((.def_702 (<= 0.0 .def_687)))
+(let ((.def_703 (not .def_702)))
+(let ((.def_876 (or .def_703 .def_849)))
+(let ((.def_879 (and .def_876 .def_878)))
+(let ((.def_874 (or .def_739 .def_873)))
+(let ((.def_875 (not .def_874)))
+(let ((.def_880 (or .def_875 .def_879)))
+(let ((.def_868 (not .def_849)))
+(let ((.def_869 (or .def_702 .def_868)))
+(let ((.def_689 (not .def_688)))
+(let ((.def_867 (or .def_689 .def_866)))
+(let ((.def_870 (and .def_867 .def_869)))
+(let ((.def_864 (or .def_749 .def_863)))
+(let ((.def_865 (not .def_864)))
+(let ((.def_871 (or .def_865 .def_870)))
+(let ((.def_881 (and .def_871 .def_880)))
+(let ((.def_850 (and .def_702 .def_849)))
+(let ((.def_882 (and .def_850 .def_881)))
+(let ((.def_923 (and .def_882 .def_922)))
+(let ((.def_715 (* 2.0 .def_650)))
+(let ((.def_794 (* (- 1.0) .def_715)))
+(let ((.def_795 (* m.delta__AT1 .def_794)))
+(let ((.def_796 (* 50.0 .def_795)))
+(let ((.def_801 (+ .def_720 .def_796)))
+(let ((.def_802 (+ .def_718 .def_801)))
+(let ((.def_803 (+ .def_722 .def_802)))
+(let ((.def_804 (+ .def_724 .def_803)))
+(let ((.def_807 (<= .def_804 0.0 )))
+(let ((.def_814 (not .def_807)))
+(let ((.def_815 (or .def_738 .def_814)))
+(let ((.def_805 (<= 0.0 .def_804)))
+(let ((.def_813 (or .def_749 .def_805)))
+(let ((.def_816 (and .def_813 .def_815)))
+(let ((.def_817 (or .def_771 .def_816)))
+(let ((.def_809 (not .def_805)))
+(let ((.def_810 (or .def_748 .def_809)))
+(let ((.def_808 (or .def_739 .def_807)))
+(let ((.def_811 (and .def_808 .def_810)))
+(let ((.def_812 (or .def_781 .def_811)))
+(let ((.def_818 (and .def_812 .def_817)))
+(let ((.def_806 (and .def_748 .def_805)))
+(let ((.def_819 (and .def_806 .def_818)))
+(let ((.def_820 (and .def_792 .def_819)))
+(let ((.def_716 (* m.delta__AT1 .def_715)))
+(let ((.def_717 (* (- 50.0) .def_716)))
+(let ((.def_726 (+ .def_720 .def_717)))
+(let ((.def_727 (+ .def_718 .def_726)))
+(let ((.def_728 (+ .def_722 .def_727)))
+(let ((.def_729 (+ .def_724 .def_728)))
+(let ((.def_746 (<= 0.0 .def_729)))
+(let ((.def_747 (not .def_746)))
+(let ((.def_774 (or .def_747 .def_748)))
+(let ((.def_730 (<= .def_729 0.0 )))
+(let ((.def_773 (or .def_730 .def_739)))
+(let ((.def_775 (and .def_773 .def_774)))
+(let ((.def_782 (or .def_775 .def_781)))
+(let ((.def_731 (not .def_730)))
+(let ((.def_760 (or .def_731 .def_738)))
+(let ((.def_759 (or .def_746 .def_749)))
+(let ((.def_761 (and .def_759 .def_760)))
+(let ((.def_772 (or .def_761 .def_771)))
+(let ((.def_783 (and .def_772 .def_782)))
+(let ((.def_758 (and .def_730 .def_738)))
+(let ((.def_784 (and .def_758 .def_783)))
+(let ((.def_793 (and .def_784 .def_792)))
+(let ((.def_821 (or .def_793 .def_820)))
+(let ((.def_662 (* m.delta__AT1 .def_661)))
+(let ((.def_663 (* (- 25.0) .def_662)))
+(let ((.def_658 (* m.delta__AT1 .def_657)))
+(let ((.def_659 (* (- 50.0) .def_658)))
+(let ((.def_673 (+ .def_659 .def_663)))
+(let ((.def_654 (* m.delta__AT1 .def_653)))
+(let ((.def_655 (* (- 25.0) .def_654)))
+(let ((.def_674 (+ .def_655 .def_673)))
+(let ((.def_651 (* .def_600 .def_650)))
+(let ((.def_652 (* (- 50.0) .def_651)))
+(let ((.def_675 (+ .def_652 .def_674)))
+(let ((.def_676 (+ .def_669 .def_675)))
+(let ((.def_677 (+ .def_667 .def_676)))
+(let ((.def_678 (+ .def_665 .def_677)))
+(let ((.def_679 (+ .def_671 .def_678)))
+(let ((.def_700 (<= 0.0 .def_679)))
+(let ((.def_701 (not .def_700)))
+(let ((.def_753 (or .def_701 .def_702)))
+(let ((.def_680 (<= .def_679 0.0 )))
+(let ((.def_752 (or .def_680 .def_689)))
+(let ((.def_754 (and .def_752 .def_753)))
+(let ((.def_750 (or .def_747 .def_749)))
+(let ((.def_751 (not .def_750)))
+(let ((.def_755 (or .def_751 .def_754)))
+(let ((.def_681 (not .def_680)))
+(let ((.def_743 (or .def_681 .def_688)))
+(let ((.def_742 (or .def_700 .def_703)))
+(let ((.def_744 (and .def_742 .def_743)))
+(let ((.def_740 (or .def_731 .def_739)))
+(let ((.def_741 (not .def_740)))
+(let ((.def_745 (or .def_741 .def_744)))
+(let ((.def_756 (and .def_745 .def_755)))
+(let ((.def_714 (and .def_680 .def_688)))
+(let ((.def_757 (and .def_714 .def_756)))
+(let ((.def_822 (and .def_757 .def_821)))
+(let ((.def_924 (or .def_822 .def_923)))
+(let ((.def_628 (* (- 20.0) m.speed_x__AT1)))
+(let ((.def_629 (* m.delta__AT1 .def_628)))
+(let ((.def_630 (* (- 200.0) .def_629)))
+(let ((.def_625 (* m.delta__AT1 .def_624)))
+(let ((.def_626 (* (- 200.0) .def_625)))
+(let ((.def_638 (+ .def_626 .def_630)))
+(let ((.def_621 (* .def_600 .def_620)))
+(let ((.def_622 (* (- 100.0) .def_621)))
+(let ((.def_639 (+ .def_622 .def_638)))
+(let ((.def_617 (* m.delta__AT1 .def_616)))
+(let ((.def_618 (* (- 200.0) .def_617)))
+(let ((.def_640 (+ .def_618 .def_639)))
+(let ((.def_613 (* .def_600 .def_612)))
+(let ((.def_614 (* (- 200.0) .def_613)))
+(let ((.def_641 (+ .def_614 .def_640)))
+(let ((.def_609 (* .def_600 .def_608)))
+(let ((.def_610 (* (- 100.0) .def_609)))
+(let ((.def_642 (+ .def_610 .def_641)))
+(let ((.def_605 (* .def_601 .def_604)))
+(let ((.def_606 (* (- 200.0) .def_605)))
+(let ((.def_643 (+ .def_606 .def_642)))
+(let ((.def_602 (* m.delta__AT1 .def_601)))
+(let ((.def_603 (* (- 2401.0) .def_602)))
+(let ((.def_644 (+ .def_603 .def_643)))
+(let ((.def_593 (* m.x__AT1 m.x__AT1)))
+(let ((.def_634 (* (- 100.0) .def_593)))
+(let ((.def_645 (+ .def_634 .def_644)))
+(let ((.def_555 (* m.y__AT1 m.y__AT1)))
+(let ((.def_632 (* (- 100.0) .def_555)))
+(let ((.def_646 (+ .def_632 .def_645)))
+(let ((.def_636 (* 4000.0 m.x__AT1)))
+(let ((.def_647 (+ .def_636 .def_646)))
+(let ((.def_694 (<= 0.0 .def_647)))
+(let ((.def_708 (not .def_694)))
+(let ((.def_594 (* (- 1.0) .def_593)))
+(let ((.def_592 (* (- 1.0) .def_555)))
+(let ((.def_595 (+ .def_592 .def_594)))
+(let ((.def_596 (* 40.0 m.x__AT1)))
+(let ((.def_598 (+ .def_596 .def_595)))
+(let ((.def_692 (<= 0.0 .def_598)))
+(let ((.def_709 (or .def_692 .def_708)))
+(let ((.def_599 (<= .def_598 0.0 )))
+(let ((.def_706 (not .def_599)))
+(let ((.def_648 (<= .def_647 0.0 )))
+(let ((.def_707 (or .def_648 .def_706)))
+(let ((.def_710 (and .def_707 .def_709)))
+(let ((.def_704 (or .def_701 .def_703)))
+(let ((.def_705 (not .def_704)))
+(let ((.def_711 (or .def_705 .def_710)))
+(let ((.def_696 (not .def_648)))
+(let ((.def_697 (or .def_599 .def_696)))
+(let ((.def_693 (not .def_692)))
+(let ((.def_695 (or .def_693 .def_694)))
+(let ((.def_698 (and .def_695 .def_697)))
+(let ((.def_690 (or .def_681 .def_689)))
+(let ((.def_691 (not .def_690)))
+(let ((.def_699 (or .def_691 .def_698)))
+(let ((.def_712 (and .def_699 .def_711)))
+(let ((.def_649 (and .def_599 .def_648)))
+(let ((.def_713 (and .def_649 .def_712)))
+(let ((.def_925 (and .def_713 .def_924)))
+(let ((.def_952 (and .def_925 .def_951)))
+(let ((.def_972 (and .def_952 .def_971)))
+(let ((.def_571 (+ m.x__AT1 .def_570)))
+(let ((.def_577 (<= .def_571 0.0 )))
+(let ((.def_586 (not .def_577)))
+(let ((.def_575 (<= m.x__AT1 0.0 )))
+(let ((.def_587 (or .def_575 .def_586)))
+(let ((.def_558 (<= 0.0 m.x__AT1)))
+(let ((.def_584 (not .def_558)))
+(let ((.def_572 (<= 0.0 .def_571)))
+(let ((.def_585 (or .def_572 .def_584)))
+(let ((.def_588 (and .def_585 .def_587)))
+(let ((.def_583 (<= m.speed_x__AT1 0.0 )))
+(let ((.def_589 (or .def_583 .def_588)))
+(let ((.def_579 (not .def_572)))
+(let ((.def_580 (or .def_558 .def_579)))
+(let ((.def_576 (not .def_575)))
+(let ((.def_578 (or .def_576 .def_577)))
+(let ((.def_581 (and .def_578 .def_580)))
+(let ((.def_574 (<= 0.0 m.speed_x__AT1)))
+(let ((.def_582 (or .def_574 .def_581)))
+(let ((.def_590 (and .def_582 .def_589)))
+(let ((.def_573 (and .def_558 .def_572)))
+(let ((.def_591 (and .def_573 .def_590)))
+(let ((.def_973 (and .def_591 .def_972)))
+(let ((.def_566 (<= m.x__AT0 20.0 )))
+(let ((.def_562 (and .def_560 .def_561)))
+(let ((.def_553 (+ (- 20.0) m.x__AT1)))
+(let ((.def_554 (* .def_553 .def_553)))
+(let ((.def_556 (+ .def_554 .def_555)))
+(let ((.def_557 (<= 400.0 .def_556)))
+(let ((.def_559 (and .def_557 .def_558)))
+(let ((.def_563 (and .def_559 .def_562)))
+(let ((.def_552 (or .def_549 .def_551)))
+(let ((.def_564 (and .def_552 .def_563)))
+(let ((.def_543 (<= 0.0 m.delta__AT0)))
+(let ((.def_27 (not m.EVENT.0__AT0)))
+(let ((.def_25 (not m.EVENT.1__AT0)))
+(let ((.def_476 (and .def_25 .def_27)))
+(let ((.def_478 (not .def_476)))
+(let ((.def_544 (or .def_478 .def_543)))
+(let ((.def_545 (or m.EVENT.1__AT0 .def_544)))
+(let ((.def_532 (* (- 10.0) m.y__AT1)))
+(let ((.def_428 (* m.speed_y__AT0 m.delta__AT0)))
+(let ((.def_429 (* 10.0 .def_428)))
+(let ((.def_535 (+ .def_429 .def_532)))
+(let ((.def_79 (* m.delta__AT0 m.delta__AT0)))
+(let ((.def_427 (* (- 49.0) .def_79)))
+(let ((.def_536 (+ .def_427 .def_535)))
+(let ((.def_431 (* 10.0 m.y__AT0)))
+(let ((.def_537 (+ .def_431 .def_536)))
+(let ((.def_538 (= .def_537 0.0 )))
+(let ((.def_526 (* (- 5.0) m.speed_y__AT1)))
+(let ((.def_264 (* (- 49.0) m.delta__AT0)))
+(let ((.def_527 (+ .def_264 .def_526)))
+(let ((.def_265 (* 5.0 m.speed_y__AT0)))
+(let ((.def_528 (+ .def_265 .def_527)))
+(let ((.def_529 (= .def_528 0.0 )))
+(let ((.def_47 (* m.speed_x__AT0 m.delta__AT0)))
+(let ((.def_522 (+ .def_47 .def_521)))
+(let ((.def_523 (+ m.x__AT0 .def_522)))
+(let ((.def_524 (= .def_523 0.0 )))
+(let ((.def_502 (= m.speed_x__AT0 m.speed_x__AT1)))
+(let ((.def_525 (and .def_502 .def_524)))
+(let ((.def_530 (and .def_525 .def_529)))
+(let ((.def_539 (and .def_530 .def_538)))
+(let ((.def_540 (or .def_478 .def_539)))
+(let ((.def_515 (= m.delta__AT0 0.0 )))
+(let ((.def_516 (and .def_476 .def_515)))
+(let ((.def_517 (not .def_516)))
+(let ((.def_499 (= m.y__AT0 m.y__AT1)))
+(let ((.def_496 (= m.x__AT0 m.x__AT1)))
+(let ((.def_510 (and .def_496 .def_499)))
+(let ((.def_511 (and .def_502 .def_510)))
+(let ((.def_505 (= m.speed_y__AT0 m.speed_y__AT1)))
+(let ((.def_512 (and .def_505 .def_511)))
+(let ((.def_518 (or .def_512 .def_517)))
+(let ((.def_519 (or m.EVENT.1__AT0 .def_518)))
+(let ((.def_513 (or .def_476 .def_512)))
+(let ((.def_514 (or m.EVENT.1__AT0 .def_513)))
+(let ((.def_520 (and .def_514 .def_519)))
+(let ((.def_541 (and .def_520 .def_540)))
+(let ((.def_483 (= m.time__AT0 m.time__AT1)))
+(let ((.def_497 (and .def_483 .def_496)))
+(let ((.def_500 (and .def_497 .def_499)))
+(let ((.def_503 (and .def_500 .def_502)))
+(let ((.def_506 (and .def_503 .def_505)))
+(let ((.def_507 (or .def_25 .def_506)))
+(let ((.def_486 (* (- 1.0) m.time__AT1)))
+(let ((.def_489 (+ m.delta__AT0 .def_486)))
+(let ((.def_490 (+ m.time__AT0 .def_489)))
+(let ((.def_491 (= .def_490 0.0 )))
+(let ((.def_492 (or .def_478 .def_491)))
+(let ((.def_493 (or m.EVENT.1__AT0 .def_492)))
+(let ((.def_484 (or .def_476 .def_483)))
+(let ((.def_485 (or m.EVENT.1__AT0 .def_484)))
+(let ((.def_494 (and .def_485 .def_493)))
+(let ((.def_508 (and .def_494 .def_507)))
+(let ((.def_480 (= .def_478 m.event_is_timed__AT1)))
+(let ((.def_477 (= m.event_is_timed__AT0 .def_476)))
+(let ((.def_481 (and .def_477 .def_480)))
+(let ((.def_509 (and .def_481 .def_508)))
+(let ((.def_542 (and .def_509 .def_541)))
+(let ((.def_546 (and .def_542 .def_545)))
+(let ((.def_547 (and .def_25 .def_546)))
+(let ((.def_565 (and .def_547 .def_564)))
+(let ((.def_567 (and .def_565 .def_566)))
+(let ((.def_430 (+ .def_427 .def_429)))
+(let ((.def_433 (+ .def_431 .def_430)))
+(let ((.def_458 (<= .def_433 0.0 )))
+(let ((.def_466 (not .def_458)))
+(let ((.def_456 (<= m.y__AT0 0.0 )))
+(let ((.def_467 (or .def_456 .def_466)))
+(let ((.def_40 (<= 0.0 m.y__AT0)))
+(let ((.def_464 (not .def_40)))
+(let ((.def_454 (<= 0.0 .def_433)))
+(let ((.def_465 (or .def_454 .def_464)))
+(let ((.def_468 (and .def_465 .def_467)))
+(let ((.def_270 (<= m.speed_y__AT0 0.0 )))
+(let ((.def_271 (not .def_270)))
+(let ((.def_267 (+ .def_265 .def_264)))
+(let ((.def_268 (<= .def_267 0.0 )))
+(let ((.def_269 (not .def_268)))
+(let ((.def_272 (or .def_269 .def_271)))
+(let ((.def_273 (not .def_272)))
+(let ((.def_469 (or .def_273 .def_468)))
+(let ((.def_460 (not .def_454)))
+(let ((.def_461 (or .def_40 .def_460)))
+(let ((.def_457 (not .def_456)))
+(let ((.def_459 (or .def_457 .def_458)))
+(let ((.def_462 (and .def_459 .def_461)))
+(let ((.def_279 (<= 0.0 .def_267)))
+(let ((.def_280 (not .def_279)))
+(let ((.def_22 (<= 0.0 m.speed_y__AT0)))
+(let ((.def_278 (not .def_22)))
+(let ((.def_281 (or .def_278 .def_280)))
+(let ((.def_282 (not .def_281)))
+(let ((.def_463 (or .def_282 .def_462)))
+(let ((.def_470 (and .def_463 .def_469)))
+(let ((.def_455 (and .def_40 .def_454)))
+(let ((.def_471 (and .def_455 .def_470)))
+(let ((.def_291 (and .def_268 .def_270)))
+(let ((.def_288 (or .def_22 .def_280)))
+(let ((.def_287 (or .def_268 .def_271)))
+(let ((.def_289 (and .def_287 .def_288)))
+(let ((.def_292 (and .def_289 .def_291)))
+(let ((.def_286 (and .def_22 .def_279)))
+(let ((.def_290 (and .def_286 .def_289)))
+(let ((.def_293 (or .def_290 .def_292)))
+(let ((.def_472 (and .def_293 .def_471)))
+(let ((.def_434 (<= .def_433 1000.0 )))
+(let ((.def_446 (not .def_434)))
+(let ((.def_39 (<= m.y__AT0 100.0 )))
+(let ((.def_447 (or .def_39 .def_446)))
+(let ((.def_440 (<= 100.0 m.y__AT0)))
+(let ((.def_444 (not .def_440)))
+(let ((.def_438 (<= 1000.0 .def_433)))
+(let ((.def_445 (or .def_438 .def_444)))
+(let ((.def_448 (and .def_445 .def_447)))
+(let ((.def_449 (or .def_273 .def_448)))
+(let ((.def_439 (not .def_438)))
+(let ((.def_441 (or .def_439 .def_440)))
+(let ((.def_436 (not .def_39)))
+(let ((.def_437 (or .def_434 .def_436)))
+(let ((.def_442 (and .def_437 .def_441)))
+(let ((.def_443 (or .def_282 .def_442)))
+(let ((.def_450 (and .def_443 .def_449)))
+(let ((.def_435 (and .def_39 .def_434)))
+(let ((.def_451 (and .def_435 .def_450)))
+(let ((.def_452 (and .def_293 .def_451)))
+(let ((.def_89 (* (- (/ 49 10)) m.speed_y__AT0)))
+(let ((.def_140 (* 3.0 .def_89)))
+(let ((.def_324 (* (- 1.0) .def_140)))
+(let ((.def_352 (* 2.0 .def_324)))
+(let ((.def_396 (* (- 1.0) .def_352)))
+(let ((.def_397 (* m.delta__AT0 .def_396)))
+(let ((.def_398 (* (- 50.0) .def_397)))
+(let ((.def_108 (* m.speed_x__AT0 m.speed_x__AT0)))
+(let ((.def_216 (* (- 50.0) .def_108)))
+(let ((.def_403 (+ .def_216 .def_398)))
+(let ((.def_95 (* m.speed_y__AT0 m.speed_y__AT0)))
+(let ((.def_214 (* (- 50.0) .def_95)))
+(let ((.def_404 (+ .def_214 .def_403)))
+(let ((.def_220 (* (- 7203.0) .def_79)))
+(let ((.def_405 (+ .def_220 .def_404)))
+(let ((.def_223 (* 490.0 m.y__AT0)))
+(let ((.def_406 (+ .def_223 .def_405)))
+(let ((.def_409 (<= 0.0 .def_406)))
+(let ((.def_416 (not .def_409)))
+(let ((.def_234 (* (- 5.0) .def_108)))
+(let ((.def_233 (* (- 5.0) .def_95)))
+(let ((.def_235 (+ .def_233 .def_234)))
+(let ((.def_236 (* 49.0 m.y__AT0)))
+(let ((.def_238 (+ .def_236 .def_235)))
+(let ((.def_249 (<= 0.0 .def_238)))
+(let ((.def_417 (or .def_249 .def_416)))
+(let ((.def_407 (<= .def_406 0.0 )))
+(let ((.def_239 (<= .def_238 0.0 )))
+(let ((.def_240 (not .def_239)))
+(let ((.def_415 (or .def_240 .def_407)))
+(let ((.def_418 (and .def_415 .def_417)))
+(let ((.def_419 (or .def_282 .def_418)))
+(let ((.def_411 (not .def_407)))
+(let ((.def_412 (or .def_239 .def_411)))
+(let ((.def_250 (not .def_249)))
+(let ((.def_410 (or .def_250 .def_409)))
+(let ((.def_413 (and .def_410 .def_412)))
+(let ((.def_414 (or .def_273 .def_413)))
+(let ((.def_420 (and .def_414 .def_419)))
+(let ((.def_408 (and .def_239 .def_407)))
+(let ((.def_421 (and .def_408 .def_420)))
+(let ((.def_422 (and .def_293 .def_421)))
+(let ((.def_353 (* m.delta__AT0 .def_352)))
+(let ((.def_354 (* 50.0 .def_353)))
+(let ((.def_359 (+ .def_216 .def_354)))
+(let ((.def_360 (+ .def_214 .def_359)))
+(let ((.def_361 (+ .def_220 .def_360)))
+(let ((.def_362 (+ .def_223 .def_361)))
+(let ((.def_373 (<= .def_362 0.0 )))
+(let ((.def_374 (not .def_373)))
+(let ((.def_390 (or .def_239 .def_374)))
+(let ((.def_363 (<= 0.0 .def_362)))
+(let ((.def_389 (or .def_250 .def_363)))
+(let ((.def_391 (and .def_389 .def_390)))
+(let ((.def_392 (or .def_273 .def_391)))
+(let ((.def_364 (not .def_363)))
+(let ((.def_386 (or .def_249 .def_364)))
+(let ((.def_385 (or .def_240 .def_373)))
+(let ((.def_387 (and .def_385 .def_386)))
+(let ((.def_388 (or .def_282 .def_387)))
+(let ((.def_393 (and .def_388 .def_392)))
+(let ((.def_384 (and .def_249 .def_363)))
+(let ((.def_394 (and .def_384 .def_393)))
+(let ((.def_395 (and .def_293 .def_394)))
+(let ((.def_423 (or .def_395 .def_422)))
+(let ((.def_156 (* 2.0 .def_108)))
+(let ((.def_336 (* (- 1.0) .def_156)))
+(let ((.def_337 (* m.delta__AT0 .def_336)))
+(let ((.def_338 (* 25.0 .def_337)))
+(let ((.def_100 (* (- (/ 49 10)) m.y__AT0)))
+(let ((.def_152 (* 2.0 .def_100)))
+(let ((.def_332 (* (- 1.0) .def_152)))
+(let ((.def_333 (* m.delta__AT0 .def_332)))
+(let ((.def_334 (* 50.0 .def_333)))
+(let ((.def_343 (+ .def_334 .def_338)))
+(let ((.def_146 (* 2.0 .def_95)))
+(let ((.def_328 (* (- 1.0) .def_146)))
+(let ((.def_329 (* m.delta__AT0 .def_328)))
+(let ((.def_330 (* 25.0 .def_329)))
+(let ((.def_344 (+ .def_330 .def_343)))
+(let ((.def_325 (* .def_79 .def_324)))
+(let ((.def_326 (* 50.0 .def_325)))
+(let ((.def_345 (+ .def_326 .def_344)))
+(let ((.def_112 (* m.x__AT0 m.speed_x__AT0)))
+(let ((.def_164 (* (- 50.0) .def_112)))
+(let ((.def_346 (+ .def_164 .def_345)))
+(let ((.def_104 (* m.y__AT0 m.speed_y__AT0)))
+(let ((.def_162 (* (- 50.0) .def_104)))
+(let ((.def_347 (+ .def_162 .def_346)))
+(let ((.def_80 (* m.delta__AT0 .def_79)))
+(let ((.def_160 (* (- 2401.0) .def_80)))
+(let ((.def_348 (+ .def_160 .def_347)))
+(let ((.def_167 (* 1000.0 m.speed_x__AT0)))
+(let ((.def_349 (+ .def_167 .def_348)))
+(let ((.def_367 (<= .def_349 0.0 )))
+(let ((.def_378 (not .def_367)))
+(let ((.def_179 (* (- 1.0) .def_112)))
+(let ((.def_178 (* (- 1.0) .def_104)))
+(let ((.def_180 (+ .def_178 .def_179)))
+(let ((.def_181 (* 20.0 m.speed_x__AT0)))
+(let ((.def_183 (+ .def_181 .def_180)))
+(let ((.def_184 (<= .def_183 0.0 )))
+(let ((.def_379 (or .def_184 .def_378)))
+(let ((.def_350 (<= 0.0 .def_349)))
+(let ((.def_198 (<= 0.0 .def_183)))
+(let ((.def_199 (not .def_198)))
+(let ((.def_377 (or .def_199 .def_350)))
+(let ((.def_380 (and .def_377 .def_379)))
+(let ((.def_375 (or .def_240 .def_374)))
+(let ((.def_376 (not .def_375)))
+(let ((.def_381 (or .def_376 .def_380)))
+(let ((.def_369 (not .def_350)))
+(let ((.def_370 (or .def_198 .def_369)))
+(let ((.def_185 (not .def_184)))
+(let ((.def_368 (or .def_185 .def_367)))
+(let ((.def_371 (and .def_368 .def_370)))
+(let ((.def_365 (or .def_250 .def_364)))
+(let ((.def_366 (not .def_365)))
+(let ((.def_372 (or .def_366 .def_371)))
+(let ((.def_382 (and .def_372 .def_381)))
+(let ((.def_351 (and .def_198 .def_350)))
+(let ((.def_383 (and .def_351 .def_382)))
+(let ((.def_424 (and .def_383 .def_423)))
+(let ((.def_211 (* 2.0 .def_140)))
+(let ((.def_295 (* (- 1.0) .def_211)))
+(let ((.def_296 (* m.delta__AT0 .def_295)))
+(let ((.def_297 (* 50.0 .def_296)))
+(let ((.def_302 (+ .def_216 .def_297)))
+(let ((.def_303 (+ .def_214 .def_302)))
+(let ((.def_304 (+ .def_220 .def_303)))
+(let ((.def_305 (+ .def_223 .def_304)))
+(let ((.def_308 (<= .def_305 0.0 )))
+(let ((.def_315 (not .def_308)))
+(let ((.def_316 (or .def_239 .def_315)))
+(let ((.def_306 (<= 0.0 .def_305)))
+(let ((.def_314 (or .def_250 .def_306)))
+(let ((.def_317 (and .def_314 .def_316)))
+(let ((.def_318 (or .def_273 .def_317)))
+(let ((.def_310 (not .def_306)))
+(let ((.def_311 (or .def_249 .def_310)))
+(let ((.def_309 (or .def_240 .def_308)))
+(let ((.def_312 (and .def_309 .def_311)))
+(let ((.def_313 (or .def_282 .def_312)))
+(let ((.def_319 (and .def_313 .def_318)))
+(let ((.def_307 (and .def_249 .def_306)))
+(let ((.def_320 (and .def_307 .def_319)))
+(let ((.def_321 (and .def_293 .def_320)))
+(let ((.def_212 (* m.delta__AT0 .def_211)))
+(let ((.def_213 (* (- 50.0) .def_212)))
+(let ((.def_225 (+ .def_216 .def_213)))
+(let ((.def_226 (+ .def_214 .def_225)))
+(let ((.def_227 (+ .def_220 .def_226)))
+(let ((.def_228 (+ .def_223 .def_227)))
+(let ((.def_247 (<= 0.0 .def_228)))
+(let ((.def_248 (not .def_247)))
+(let ((.def_276 (or .def_248 .def_249)))
+(let ((.def_229 (<= .def_228 0.0 )))
+(let ((.def_275 (or .def_229 .def_240)))
+(let ((.def_277 (and .def_275 .def_276)))
+(let ((.def_283 (or .def_277 .def_282)))
+(let ((.def_230 (not .def_229)))
+(let ((.def_261 (or .def_230 .def_239)))
+(let ((.def_260 (or .def_247 .def_250)))
+(let ((.def_262 (and .def_260 .def_261)))
+(let ((.def_274 (or .def_262 .def_273)))
+(let ((.def_284 (and .def_274 .def_283)))
+(let ((.def_259 (and .def_229 .def_239)))
+(let ((.def_285 (and .def_259 .def_284)))
+(let ((.def_294 (and .def_285 .def_293)))
+(let ((.def_322 (or .def_294 .def_321)))
+(let ((.def_157 (* m.delta__AT0 .def_156)))
+(let ((.def_158 (* (- 25.0) .def_157)))
+(let ((.def_153 (* m.delta__AT0 .def_152)))
+(let ((.def_154 (* (- 50.0) .def_153)))
+(let ((.def_169 (+ .def_154 .def_158)))
+(let ((.def_147 (* m.delta__AT0 .def_146)))
+(let ((.def_150 (* (- 25.0) .def_147)))
+(let ((.def_170 (+ .def_150 .def_169)))
+(let ((.def_141 (* .def_79 .def_140)))
+(let ((.def_144 (* (- 50.0) .def_141)))
+(let ((.def_171 (+ .def_144 .def_170)))
+(let ((.def_172 (+ .def_164 .def_171)))
+(let ((.def_173 (+ .def_162 .def_172)))
+(let ((.def_174 (+ .def_160 .def_173)))
+(let ((.def_175 (+ .def_167 .def_174)))
+(let ((.def_196 (<= 0.0 .def_175)))
+(let ((.def_197 (not .def_196)))
+(let ((.def_254 (or .def_197 .def_198)))
+(let ((.def_176 (<= .def_175 0.0 )))
+(let ((.def_253 (or .def_176 .def_185)))
+(let ((.def_255 (and .def_253 .def_254)))
+(let ((.def_251 (or .def_248 .def_250)))
+(let ((.def_252 (not .def_251)))
+(let ((.def_256 (or .def_252 .def_255)))
+(let ((.def_177 (not .def_176)))
+(let ((.def_244 (or .def_177 .def_184)))
+(let ((.def_243 (or .def_196 .def_199)))
+(let ((.def_245 (and .def_243 .def_244)))
+(let ((.def_241 (or .def_230 .def_240)))
+(let ((.def_242 (not .def_241)))
+(let ((.def_246 (or .def_242 .def_245)))
+(let ((.def_257 (and .def_246 .def_256)))
+(let ((.def_210 (and .def_176 .def_184)))
+(let ((.def_258 (and .def_210 .def_257)))
+(let ((.def_323 (and .def_258 .def_322)))
+(let ((.def_425 (or .def_323 .def_424)))
+(let ((.def_116 (* (- 20.0) m.speed_x__AT0)))
+(let ((.def_117 (* m.delta__AT0 .def_116)))
+(let ((.def_118 (* (- 200.0) .def_117)))
+(let ((.def_113 (* m.delta__AT0 .def_112)))
+(let ((.def_114 (* (- 200.0) .def_113)))
+(let ((.def_127 (+ .def_114 .def_118)))
+(let ((.def_109 (* .def_79 .def_108)))
+(let ((.def_110 (* (- 100.0) .def_109)))
+(let ((.def_128 (+ .def_110 .def_127)))
+(let ((.def_105 (* m.delta__AT0 .def_104)))
+(let ((.def_106 (* (- 200.0) .def_105)))
+(let ((.def_129 (+ .def_106 .def_128)))
+(let ((.def_101 (* .def_79 .def_100)))
+(let ((.def_102 (* (- 200.0) .def_101)))
+(let ((.def_130 (+ .def_102 .def_129)))
+(let ((.def_96 (* .def_79 .def_95)))
+(let ((.def_98 (* (- 100.0) .def_96)))
+(let ((.def_131 (+ .def_98 .def_130)))
+(let ((.def_90 (* .def_80 .def_89)))
+(let ((.def_93 (* (- 200.0) .def_90)))
+(let ((.def_132 (+ .def_93 .def_131)))
+(let ((.def_81 (* m.delta__AT0 .def_80)))
+(let ((.def_84 (* (- 2401.0) .def_81)))
+(let ((.def_133 (+ .def_84 .def_132)))
+(let ((.def_71 (* m.x__AT0 m.x__AT0)))
+(let ((.def_122 (* (- 100.0) .def_71)))
+(let ((.def_134 (+ .def_122 .def_133)))
+(let ((.def_32 (* m.y__AT0 m.y__AT0)))
+(let ((.def_120 (* (- 100.0) .def_32)))
+(let ((.def_135 (+ .def_120 .def_134)))
+(let ((.def_125 (* 4000.0 m.x__AT0)))
+(let ((.def_136 (+ .def_125 .def_135)))
+(let ((.def_190 (<= 0.0 .def_136)))
+(let ((.def_204 (not .def_190)))
+(let ((.def_72 (* (- 1.0) .def_71)))
+(let ((.def_70 (* (- 1.0) .def_32)))
+(let ((.def_73 (+ .def_70 .def_72)))
+(let ((.def_75 (* 40.0 m.x__AT0)))
+(let ((.def_77 (+ .def_75 .def_73)))
+(let ((.def_188 (<= 0.0 .def_77)))
+(let ((.def_205 (or .def_188 .def_204)))
+(let ((.def_78 (<= .def_77 0.0 )))
+(let ((.def_202 (not .def_78)))
+(let ((.def_137 (<= .def_136 0.0 )))
+(let ((.def_203 (or .def_137 .def_202)))
+(let ((.def_206 (and .def_203 .def_205)))
+(let ((.def_200 (or .def_197 .def_199)))
+(let ((.def_201 (not .def_200)))
+(let ((.def_207 (or .def_201 .def_206)))
+(let ((.def_192 (not .def_137)))
+(let ((.def_193 (or .def_78 .def_192)))
+(let ((.def_189 (not .def_188)))
+(let ((.def_191 (or .def_189 .def_190)))
+(let ((.def_194 (and .def_191 .def_193)))
+(let ((.def_186 (or .def_177 .def_185)))
+(let ((.def_187 (not .def_186)))
+(let ((.def_195 (or .def_187 .def_194)))
+(let ((.def_208 (and .def_195 .def_207)))
+(let ((.def_138 (and .def_78 .def_137)))
+(let ((.def_209 (and .def_138 .def_208)))
+(let ((.def_426 (and .def_209 .def_425)))
+(let ((.def_453 (and .def_426 .def_452)))
+(let ((.def_473 (and .def_453 .def_472)))
+(let ((.def_48 (+ m.x__AT0 .def_47)))
+(let ((.def_53 (<= .def_48 0.0 )))
+(let ((.def_62 (not .def_53)))
+(let ((.def_51 (<= m.x__AT0 0.0 )))
+(let ((.def_63 (or .def_51 .def_62)))
+(let ((.def_36 (<= 0.0 m.x__AT0)))
+(let ((.def_60 (not .def_36)))
+(let ((.def_49 (<= 0.0 .def_48)))
+(let ((.def_61 (or .def_49 .def_60)))
+(let ((.def_64 (and .def_61 .def_63)))
+(let ((.def_59 (<= m.speed_x__AT0 0.0 )))
+(let ((.def_65 (or .def_59 .def_64)))
+(let ((.def_55 (not .def_49)))
+(let ((.def_56 (or .def_36 .def_55)))
+(let ((.def_52 (not .def_51)))
+(let ((.def_54 (or .def_52 .def_53)))
+(let ((.def_57 (and .def_54 .def_56)))
+(let ((.def_19 (<= 0.0 m.speed_x__AT0)))
+(let ((.def_58 (or .def_19 .def_57)))
+(let ((.def_66 (and .def_58 .def_65)))
+(let ((.def_50 (and .def_36 .def_49)))
+(let ((.def_67 (and .def_50 .def_66)))
+(let ((.def_474 (and .def_67 .def_473)))
+(let ((.def_41 (and .def_39 .def_40)))
+(let ((.def_30 (+ m.x__AT0 (- 20.0) )))
+(let ((.def_31 (* .def_30 .def_30)))
+(let ((.def_33 (+ .def_31 .def_32)))
+(let ((.def_35 (<= 400.0 .def_33)))
+(let ((.def_37 (and .def_35 .def_36)))
+(let ((.def_42 (and .def_37 .def_41)))
+(let ((.def_28 (or .def_25 .def_27)))
+(let ((.def_43 (and .def_28 .def_42)))
+(let ((.def_16 (= m.y__AT0 0.0 )))
+(let ((.def_13 (= m.x__AT0 0.0 )))
+(let ((.def_9 (= m.time__AT0 0.0 )))
+(let ((.def_11 (and .def_9 m.event_is_timed__AT0)))
+(let ((.def_14 (and .def_11 .def_13)))
+(let ((.def_17 (and .def_14 .def_16)))
+(let ((.def_20 (and .def_17 .def_19)))
+(let ((.def_23 (and .def_20 .def_22)))
+(let ((.def_44 (and .def_23 .def_43)))
+(let ((.def_5 (<= m.x__AT2 20.0 )))
+(let ((.def_6 (not .def_5)))
+(let ((.def_45 (and .def_6 .def_44)))
+(let ((.def_475 (and .def_45 .def_474)))
+(let ((.def_568 (and .def_475 .def_567)))
+(let ((.def_974 (and .def_568 .def_973)))
+(let ((.def_1069 (and .def_974 .def_1068)))
+(let ((.def_1475 (and .def_1069 .def_1474)))
+.def_1475))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2.gold b/tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2.gold
new file mode 100644
index 000000000..3f65111b0
--- /dev/null
+++ b/tests/regress/mcsat/nra/simple_ballistics_reach.01.seq_lazy_lemmas_global_2.smt2.gold
@@ -0,0 +1 @@
+unsat
diff --git a/tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2 b/tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2
new file mode 100644
index 000000000..cc7de8f46
--- /dev/null
+++ b/tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2
@@ -0,0 +1,27 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :source |
+These benchmarks used in the paper:
+
+  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
+  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
+
+The meti-tarski benchmarks are proof obligations extracted from the
+Meti-Tarski project, see:
+
+  B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover
+  for real-valued special functions. Journal of Automated Reasoning,
+  44(3):175-205, 2010.
+
+Submitted by Dejan Jovanovic for SMT-LIB.
+
+
+|)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun skoX () Real)
+(declare-fun skoY () Real)
+(declare-fun pi () Real)
+(assert (let ((?v_0 (* skoX (/ (- 1) 6))) (?v_1 (* skoX (/ 1 120))) (?v_2 (* skoX (/ (- 1) 5040)))) (and (<= skoY 0) (and (not (<= (* skoY (+ (* skoX (* skoX (+ (/ 1 6) (* skoX (* skoX (+ (/ (- 1) 120) (* skoX (* skoX (+ (/ 1 5040) (* skoX (* skoX (+ (/ (- 1) 362880) (* skoX (* skoX (/ 1 39916800))))))))))))))) (* skoY (* skoY (/ (- 1) 6))))) 0)) (and (not (<= (* skoY (* skoY (+ ?v_0 (* skoY (* skoY (+ ?v_1 (* skoY (* skoY (+ ?v_2 (* skoY (* skoY (* skoX (/ 1 362880))))))))))))) (* skoX (* skoX (* skoX (+ (/ (- 1) 6) (* skoX (* skoX (+ (/ 1 120) (* skoX (* skoX (+ (/ (- 1) 5040) (* skoX (* skoX (+ (/ 1 362880) (* skoX (* skoX (/ (- 1) 39916800)))))))))))))))))) (and (not (<= (* skoY (+ (* skoX (* skoX (+ (/ 1 6) (* skoX (* skoX (+ (/ (- 1) 120) (* skoX (* skoX (/ 1 5040))))))))) (* skoY (* skoY (+ (/ (- 1) 6) (* skoY (* skoY (+ (/ 1 120) (* skoY (* skoY (+ (/ (- 1) 5040) (* skoY (* skoY (/ 1 362880)))))))))))))) 0)) (and (not (<= (* skoY (* skoY (+ ?v_0 (* skoY (* skoY ?v_1))))) (* skoX (* skoX (* skoX (+ (/ (- 1) 6) (* skoX (* skoX (+ (/ 1 120) (* skoX ?v_2)))))))))) (and (not (<= (* skoY (+ (* skoX (* skoX (/ 1 6))) (* skoY (* skoY (+ (/ (- 1) 6) (* skoY (* skoY (/ 1 120)))))))) 0)) (and (not (<= skoX 0)) (and (not (<= pi (/ 15707963 5000000))) (and (not (<= (/ 31415927 10000000) pi)) (and (<= skoY (* pi (/ 1 2))) (and (<= 0 skoX) (not (<= skoY skoX)))))))))))))))
+(check-sat)
+(exit)
diff --git a/tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2.gold b/tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2.gold
new file mode 100644
index 000000000..3f65111b0
--- /dev/null
+++ b/tests/regress/mcsat/nra/sin-problem-7-chunk-0215.smt2.gold
@@ -0,0 +1 @@
+unsat
diff --git a/tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2 b/tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2
new file mode 100644
index 000000000..eadeb0079
--- /dev/null
+++ b/tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2
@@ -0,0 +1,28 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :source |
+These benchmarks used in the paper:
+
+  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
+  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
+
+The meti-tarski benchmarks are proof obligations extracted from the
+Meti-Tarski project, see:
+
+  B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover
+  for real-valued special functions. Journal of Automated Reasoning,
+  44(3):175-205, 2010.
+
+Submitted by Dejan Jovanovic for SMT-LIB.
+
+
+|)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun skoSXY () Real)
+(declare-fun skoT () Real)
+(declare-fun skoX () Real)
+(declare-fun skoY () Real)
+(assert (and (not (= (+ (* skoSXY (- 1)) (* skoT (* skoT skoSXY))) skoX)) (and (= (+ (* skoSXY skoSXY) (* skoX (- 1))) skoY) (and (<= skoY (/ 33 32)) (and (<= skoX 2) (and (<= (/ 3 2) skoX) (and (<= 1 skoY) (and (<= 0 skoT) (<= 0 skoSXY)))))))))
+(check-sat)
+(exit)
diff --git a/tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2.gold b/tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2.gold
new file mode 100644
index 000000000..6b8a2c3d2
--- /dev/null
+++ b/tests/regress/mcsat/nra/sqrt-problem-13-chunk-0024.smt2.gold
@@ -0,0 +1 @@
+sat