diff --git a/src/mcsat/uf/uf_plugin.c b/src/mcsat/uf/uf_plugin.c
index b8411b04a..9a02803f2 100644
--- a/src/mcsat/uf/uf_plugin.c
+++ b/src/mcsat/uf/uf_plugin.c
@@ -792,7 +792,7 @@ void uf_plugin_build_model(plugin_t* plugin, model_t* model) {
       break;
     default:
       app_construct = false;
-      continue;
+      break;
     }
 
     composite_term_t* app_comp = composite_term_desc(terms, app_term);
@@ -869,10 +869,10 @@ void uf_plugin_build_model(plugin_t* plugin, model_t* model) {
 
   // Since we make functions when we see a new one, we also construct the last function
   if (app_terms.size > 0 && mappings.size > 0 && app_construct) {
-    type_t tau = get_function_application_type(terms, prev_app_kind, prev_app_f);
+    type_t tau = get_function_application_type(terms, app_kind, app_f);
     type_t range_tau = function_type_range(terms->types, tau);
     value_t f_value = vtbl_mk_function(vtbl, tau, mappings.size, mappings.data, vtbl_mk_default(terms->types, vtbl, range_tau));
-    switch (prev_app_kind) {
+    switch (app_kind) {
     case ARITH_RDIV:
       vtbl_set_zero_rdiv(vtbl, f_value);
       break;
@@ -883,7 +883,7 @@ void uf_plugin_build_model(plugin_t* plugin, model_t* model) {
       vtbl_set_zero_mod(vtbl, f_value);
       break;
     case APP_TERM:
-      model_map_term(model, prev_app_f, f_value);
+      model_map_term(model, app_f, f_value);
       break;
     default:
       assert(false);
diff --git a/tests/regress/mcsat/uf/ufnra_07.smt2 b/tests/regress/mcsat/uf/ufnra_07.smt2
new file mode 100644
index 000000000..8bb40dc8f
--- /dev/null
+++ b/tests/regress/mcsat/uf/ufnra_07.smt2
@@ -0,0 +1,16 @@
+(set-option :print-success false)
+(set-option :produce-models true)
+(set-logic QF_UFNRA)
+(declare-sort x4 0)
+(declare-fun x2 () x4)
+(declare-fun x1 () x4)
+(declare-fun x6 () Real)
+(declare-fun x3 (Real) Real)
+(declare-fun x5 () Real)
+(assert (> (* x5 2.0) x6))
+(assert (< x5 x6))
+(assert (not (= (x3 (- x6 x5)) 0.0)))
+(assert (not (not (= (x3 x6) 0.0))))
+(assert (not (= x2 x1)))
+(check-sat)
+(exit)
diff --git a/tests/regress/mcsat/uf/ufnra_07.smt2.gold b/tests/regress/mcsat/uf/ufnra_07.smt2.gold
new file mode 100644
index 000000000..30d440c39
--- /dev/null
+++ b/tests/regress/mcsat/uf/ufnra_07.smt2.gold
@@ -0,0 +1 @@
+sat
\ No newline at end of file
diff --git a/tests/regress/mcsat/uf/ufnra_07.smt2.options b/tests/regress/mcsat/uf/ufnra_07.smt2.options
new file mode 100644
index 000000000..92afff71d
--- /dev/null
+++ b/tests/regress/mcsat/uf/ufnra_07.smt2.options
@@ -0,0 +1 @@
+--mcsat --trace mcsat::model::check 
\ No newline at end of file