diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index cb52a9c85..6b53882cd 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -413,10 +413,9 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
         case generic_model_converter::instruction::HIDE:
             break;
         case generic_model_converter::instruction::ADD:
-            //            new_def = entry.m_def;
-            // (*rp)(new_def);
-            new_def = m.mk_const(entry.m_f);
-            sub->insert(new_def, new_def, nullptr, nullptr);
+            new_def = entry.m_def;
+            (*rp)(new_def);
+            sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr);
             break;
         }
     }
diff --git a/src/test/simplifier.cpp b/src/test/simplifier.cpp
index a4da49861..3b2abf7b2 100644
--- a/src/test/simplifier.cpp
+++ b/src/test/simplifier.cpp
@@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 #include "api/z3.h"
 #include "api/z3_private.h"
+#include <cstring>
 #include <iostream>
 #include "util/util.h"
 #include "util/trace.h"
@@ -211,6 +212,26 @@ static void test_array() {
     Z3_del_context(ctx);
 }
 
+static void test_sat_smt_ufbv_predicate_model_validation() {
+    Z3_context ctx = Z3_mk_context(nullptr);
+    const char* result =
+        Z3_eval_smtlib2_string(ctx,
+            "(set-logic QF_UFBV)\n"
+            "(set-option :sat.smt true)\n"
+            "(set-option :model_validate true)\n"
+            "(declare-fun p ((_ BitVec 4)) Bool)\n"
+            "(declare-const x (_ BitVec 4))\n"
+            "(declare-const y (_ BitVec 4))\n"
+            "(assert (xor (p x) (p y)))\n"
+            "(assert (bvuge x (_ bv1 4)))\n"
+            "(assert (bvult y (_ bv1 4)))\n"
+            "(check-sat)\n"
+            "(get-model)\n");
+    ENSURE(std::strstr(result, "sat") != nullptr);
+    ENSURE(std::strstr(result, "invalid model") == nullptr);
+    Z3_del_context(ctx);
+}
+
 void tst_simplifier() {
 
     test_array();
@@ -218,4 +239,5 @@ void tst_simplifier() {
     test_datatypes();
     test_bool();
     test_skolemize_bug();
+    test_sat_smt_ufbv_predicate_model_validation();
 }