diff --git a/src/mcsat/uf/uf_plugin.c b/src/mcsat/uf/uf_plugin.c
index c51612083..e1e586664 100644
--- a/src/mcsat/uf/uf_plugin.c
+++ b/src/mcsat/uf/uf_plugin.c
@@ -344,22 +344,10 @@ void uf_plugin_learn(plugin_t* plugin, trail_token_t* prop) {
     (*uf->stats.conflicts) ++;
     // extract terms used in the conflict
     term_t t;
-    term_table_t *terms = uf->ctx->terms;
-    composite_term_t* t_desc = NULL;
     uint32_t i;
     for (i = 0; i < uf->conflict.size; ++i) {
-      t = uf->conflict.data[i];
-      if (term_kind(terms, t) == EQ_TERM) {
-	t_desc = eq_term_desc(terms, t);
-      } else if (term_kind(terms, t) == BV_EQ_ATOM) {
-	t_desc = bveq_atom_desc(terms, t);
-      } else if (term_kind(terms, t) == ARITH_BINEQ_ATOM) {
-	t_desc = arith_bineq_atom_desc(terms, t);
-      } else {
-	assert(false);
-      }
-      int_mset_add(&uf->tmp, t_desc->arg[0]);
-      int_mset_add(&uf->tmp, t_desc->arg[1]);
+      t = unsigned_term(uf->conflict.data[i]);
+      int_mset_add(&uf->tmp, t);
     }
     uf_plugin_bump_terms_and_reset(uf, &uf->tmp);
     statistic_avg_add(uf->stats.avg_conflict_size, uf->conflict.size);
@@ -406,10 +394,13 @@ void uf_plugin_propagate(plugin_t* plugin, trail_token_t* prop) {
        it != NULL;
        it = int_hmap_next_record(&var_db->term_to_variable_map, it)) {
     t = it->key;
-    if (t >= 0 && eq_graph_has_term(&uf->eq_graph, t) &&
-        !eq_graph_term_has_value(&uf->eq_graph, t)) {
-      all_assigned = false;
-      break;
+    if (t >= 0 && eq_graph_has_term(&uf->eq_graph, t)) {
+      variable_t t_var = variable_db_get_variable_if_exists(var_db, t);
+      assert(t_var != variable_null);
+      if (!trail_has_value(uf->ctx->trail, t_var)) {
+        all_assigned = false;
+        break;
+      }
     }
   }
   
@@ -421,22 +412,10 @@ void uf_plugin_propagate(plugin_t* plugin, trail_token_t* prop) {
       prop->conflict(prop);
       (*uf->stats.conflicts) ++;
       // extract terms used in the conflict
-      term_table_t *terms = uf->ctx->terms;
-      composite_term_t* t_desc = NULL;
       uint32_t i;
       for (i = 0; i < uf->conflict.size; ++i) {
-        t = uf->conflict.data[i];
-	if (term_kind(terms, t) == EQ_TERM) {
-          t_desc = eq_term_desc(terms, t);
-        } else if (term_kind(terms, t) == BV_EQ_ATOM) {
-	  t_desc = bveq_atom_desc(terms, t);
-	} else if (term_kind(terms, t) == ARITH_BINEQ_ATOM) {
-	  t_desc = arith_bineq_atom_desc(terms, t);
-	} else {
-          assert(false);
-        }
-	int_mset_add(&uf->tmp, t_desc->arg[0]);
-	int_mset_add(&uf->tmp, t_desc->arg[1]);
+        t = unsigned_term(uf->conflict.data[i]);
+	int_mset_add(&uf->tmp, t);
       }
       uf_plugin_bump_terms_and_reset(uf, &uf->tmp);
       statistic_avg_add(uf->stats.avg_conflict_size, uf->conflict.size);
diff --git a/src/mcsat/weq/weak_eq_graph.c b/src/mcsat/weq/weak_eq_graph.c
index bc271182e..a0e5e9146 100644
--- a/src/mcsat/weq/weak_eq_graph.c
+++ b/src/mcsat/weq/weak_eq_graph.c
@@ -1282,20 +1282,62 @@ void copy_uniques(ivector_t *to, ivector_t *from) {
   delete_int_hset(&seen);
 }
 
+/* checks if the array terms (variable, select term, update term) are
+ * full assigned in the trail
+ */
+static
+bool weq_is_fully_assigned(const weq_graph_t* weq, term_t t) {
+  variable_t t_var = variable_db_get_variable_if_exists(weq->ctx->var_db, t);
+  assert(t_var != variable_null);
+  if (!trail_has_value(weq->ctx->trail, t_var)) {
+    return false;
+  }
+
+  const term_table_t* terms = weq->ctx->terms;
+  composite_term_t* t_desc = NULL;
+
+  switch (term_kind(terms, t)) {
+  case UNINTERPRETED_TERM:
+    // already checked
+    break;
+  case APP_TERM:
+    t_desc = app_term_desc(terms, t);
+    break;
+  case UPDATE_TERM:
+    t_desc = update_term_desc(terms, t);
+    break;
+  default:
+    assert(false);
+  }
+
+  uint32_t i;
+  for (i = 0; t_desc && i < t_desc->arity; ++ i) {
+    term_t c = t_desc->arg[i];
+    variable_t c_var = variable_db_get_variable_if_exists(weq->ctx->var_db, c);
+    assert(c_var != variable_null);
+    if (!trail_has_value(weq->ctx->trail, c_var)) {
+      return false;
+    }
+  }
+
+  return true;
+}
+
 /* filter array-eq-terms based on the current model.  We keep the
  * array terms (array variables and update terms) that have been
- * assigned a value in the equality graph. For array variables, it is
+ * assigned a value in the trail. For array variables, it is
  * just a value assigned to the variable. For update terms, we check
  * if update term, array term in the update, index term, value term
  * have been assigned a value.
  */
 static
-void filter_array_eq_terms(const weq_graph_t* weq, const term_table_t* terms,
-			   ivector_t *array_eq_terms) {
+void filter_array_eq_terms(const weq_graph_t* weq,
+                           ivector_t *array_eq_terms) {
+  const term_table_t* terms = weq->ctx->terms;
+
   uint32_t i, j;
   term_t t, arr1, arr2;
   composite_term_t* t_desc;
-  composite_term_t* update_desc;
   
   j = 0;
   for (i = 0; i < array_eq_terms->size; ++i) {
@@ -1303,29 +1345,11 @@ void filter_array_eq_terms(const weq_graph_t* weq, const term_table_t* terms,
     t_desc = eq_term_desc(terms, t);
     arr1 = t_desc->arg[0];
     arr2 = t_desc->arg[1];
-
-    if (!eq_graph_term_has_value(weq->eq_graph, arr1) ||
-	!eq_graph_term_has_value(weq->eq_graph, arr2)) {
+    if (!weq_is_fully_assigned(weq, arr1) ||
+        !weq_is_fully_assigned(weq, arr2)) {
       continue;
     }
 
-    if (term_kind(terms, arr1) == UPDATE_TERM) {
-      update_desc = update_term_desc(terms, arr1);
-      if (!eq_graph_term_has_value(weq->eq_graph, update_desc->arg[0]) ||
-	  !eq_graph_term_has_value(weq->eq_graph, update_desc->arg[1]) ||
-	  !eq_graph_term_has_value(weq->eq_graph, update_desc->arg[2])) {
-	continue;
-      }
-    }
-    if (term_kind(terms, arr2) == UPDATE_TERM) {
-      update_desc = update_term_desc(terms, arr2);
-      if (!eq_graph_term_has_value(weq->eq_graph, update_desc->arg[0]) ||
-	  !eq_graph_term_has_value(weq->eq_graph, update_desc->arg[1]) ||
-	  !eq_graph_term_has_value(weq->eq_graph, update_desc->arg[2])) {
-	continue;
-      }
-    }
-
     array_eq_terms->data[j++] = array_eq_terms->data[i];
   }
   ivector_shrink(array_eq_terms, j);
@@ -1333,34 +1357,24 @@ void filter_array_eq_terms(const weq_graph_t* weq, const term_table_t* terms,
 
 /* filter array-terms based on the current model.  We keep the
  * array terms (array variables and update terms) that have been
- * assigned a value in the equality graph. For array variables, it is
+ * assigned a value in the trail. For array variables, it is
  * just a value assigned to the variable. For update terms, we check
  * if update term, array term in the update, index term, value term
  * have been assigned a value.
  */
 static
-void filter_array_terms(const weq_graph_t* weq,	const term_table_t* terms,
-			ivector_t *array_terms) {
+void filter_array_terms(const weq_graph_t* weq,
+                        ivector_t *array_terms) {
   uint32_t i, j;
   term_t t;
-  composite_term_t* update_desc;
   
   j = 0;
   for (i = 0; i < array_terms->size; ++i) {
     t = array_terms->data[i];
-    if (!eq_graph_term_has_value(weq->eq_graph, t)) {
+    if (!weq_is_fully_assigned(weq, t)) {
       continue;
     }
 
-    if (term_kind(terms, t) == UPDATE_TERM) {
-      update_desc = update_term_desc(terms, t);
-      if (!eq_graph_term_has_value(weq->eq_graph, update_desc->arg[0]) ||
-	  !eq_graph_term_has_value(weq->eq_graph, update_desc->arg[1]) ||
-	  !eq_graph_term_has_value(weq->eq_graph, update_desc->arg[2])) {
-	continue;
-      }
-    }
-
     array_terms->data[j++] = array_terms->data[i];
   }
   ivector_shrink(array_terms, j);
@@ -1370,12 +1384,14 @@ void filter_array_terms(const weq_graph_t* weq,	const term_table_t* terms,
  * according to the current array terms.
  * Basically, we keep select terms whose first argument (i.e. an array)
  * is present in the arrays_terms vector.
- * Moreover, we filter terms that don't have values assigned in the equality graph.
+ * Moreover, we filter terms that don't have values assigned in the trail.
  */
 static
 void filter_select_terms(const weq_graph_t* weq,
-			 const term_table_t* terms, ivector_t *select_terms,
+                         ivector_t *select_terms,
                          const ivector_t *array_terms) {
+  const term_table_t* terms = weq->ctx->terms;
+
   uint32_t i, j;
   composite_term_t* select_desc;
   term_t t;
@@ -1390,13 +1406,10 @@ void filter_select_terms(const weq_graph_t* weq,
   j = 0;
   for (i = 0; i < select_terms->size; ++i) {
     t = select_terms->data[i];
-    select_desc = app_term_desc(terms, t);
-    // check if the equality graph contains model values.
-    if (!eq_graph_term_has_value(weq->eq_graph, t) ||
-	!eq_graph_term_has_value(weq->eq_graph, select_desc->arg[0]) ||
-	!eq_graph_term_has_value(weq->eq_graph, select_desc->arg[1])) {
+    if (!weq_is_fully_assigned(weq, t)) {
       continue;
     }
+    select_desc = app_term_desc(terms, t);
     
     do {
       /* The array term (first arg) in the select term can be a select
@@ -1433,19 +1446,19 @@ void weq_graph_check_array_conflict(weq_graph_t* weq, ivector_t* conflict) {
 
   init_ivector(&array_eq_terms, 0);
   copy_uniques(&array_eq_terms, &weq->array_eq_terms); 
-  filter_array_eq_terms(weq, weq->ctx->terms, &array_eq_terms);
+  filter_array_eq_terms(weq, &array_eq_terms);
 
   init_ivector(&array_terms, 0);
   copy_uniques(&array_terms, &weq->array_terms);
   // filter array terms
-  filter_array_terms(weq, weq->ctx->terms, &array_terms);
+  filter_array_terms(weq, &array_terms);
   // store array terms according to heuristic score
   int_array_sort2(array_terms.data, array_terms.size, weq->ctx, weq_graph_array_terms_compare);
   
   init_ivector(&select_terms, 0);
   copy_uniques(&select_terms, &weq->select_terms);
   // filter select terms
-  filter_select_terms(weq, weq->ctx->terms, &select_terms, &array_terms);
+  filter_select_terms(weq, &select_terms, &array_terms);
   // store select terms according to heuristic score
   int_array_sort2(select_terms.data, select_terms.size, weq->ctx, weq_graph_array_terms_compare);
 
@@ -1473,7 +1486,7 @@ void weq_graph_check_array_conflict(weq_graph_t* weq, ivector_t* conflict) {
       (*weq->stats.array_check_calls) ++;
 
       if (USE_ARRAY_DIFF) {
-	ok = weq_graph_array_ext_diff_check(weq, conflict, &array_eq_terms, NULL);
+        ok = weq_graph_array_ext_diff_check(weq, conflict, &array_eq_terms, NULL);
       }
     }