diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index ff74e4614..ed7e14b20 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -334,6 +334,52 @@ public:
     }    
 };
 
+class prefer_cmd : public cmd {
+    expr *m_formula = nullptr;
+
+public:
+    prefer_cmd() : cmd("prefer") {}
+    char const *get_usage() const override {
+        return "<formula>";
+    }
+    char const *get_descr(cmd_context &ctx) const override {
+        return "set a preferred formula for the solver";
+    }
+    unsigned get_arity() const override {
+        return 1;
+    }
+    void prepare(cmd_context &ctx) override {
+        m_formula = nullptr;
+    }
+    cmd_arg_kind next_arg_kind(cmd_context &ctx) const override {
+        return CPK_EXPR;
+    }
+    void set_next_arg(cmd_context &ctx, expr *e) override {
+        m_formula = e;
+    }
+    void execute(cmd_context &ctx) override {
+        SASSERT(m_formula);
+        ctx.set_preferred(m_formula);
+    }
+};
+
+class reset_preferences_cmd : public cmd {
+    public:
+    reset_preferences_cmd() : cmd("reset-preferences") {}
+    char const *get_usage() const override {
+        return "";
+    }
+    char const *get_descr(cmd_context &ctx) const override {
+        return "reset all preferred formulas";
+    }
+    unsigned get_arity() const override {
+        return 0;
+    }
+    void execute(cmd_context &ctx) override {
+        ctx.reset_preferred();
+    }
+};
+
 class set_get_option_cmd : public cmd {
 protected:
     symbol      m_true;
@@ -926,6 +972,8 @@ void install_basic_cmds(cmd_context & ctx) {
     ctx.insert(alloc(get_info_cmd));
     ctx.insert(alloc(set_info_cmd));
     ctx.insert(alloc(set_initial_value_cmd));
+    ctx.insert(alloc(prefer_cmd));
+    ctx.insert(alloc(reset_preferences_cmd));
     ctx.insert(alloc(get_consequences_cmd));
     ctx.insert(alloc(builtin_cmd, "assert", "<term>", "assert term."));
     ctx.insert(alloc(builtin_cmd, "check-sat", "<boolean-constants>*", "check if the current context is satisfiable. If a list of boolean constants B is provided, then check if the current context is consistent with assigning every constant in B to true."));
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 4f093e749..4af0782e1 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -628,6 +628,7 @@ cmd_context::~cmd_context() {
     finalize_tactic_manager();
     m_proof_cmds = nullptr;
     m_var2values.reset();
+    m_preferred = nullptr;
     reset(true);
     m_mcs.reset();
     m_solver = nullptr;
@@ -1518,6 +1519,8 @@ void cmd_context::reset(bool finalize) {
     m_dt_eh  = nullptr;
     m_std_subst = nullptr;
     m_rev_subst = nullptr;
+    m_preferred = nullptr;
+    m_var2values.reset();
     if (m_manager) {
         dealloc(m_pmanager);
         m_pmanager = nullptr;
@@ -1884,6 +1887,29 @@ void cmd_context::set_initial_value(expr* var, expr* value) {
     m_var2values.push_back({expr_ref(var, m()), expr_ref(value, m())});    
 }
 
+void cmd_context::set_preferred(expr* fmla) {
+    if (!m_preferred) {
+        auto p = alloc(preferred_value_propagator, m());
+        m_preferred = p;
+        if (get_solver()) {
+            get_solver()->user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh);
+            get_solver()->user_propagate_register_decide(p->decide_eh);
+        }
+    }
+    m_preferred->set_preferred(fmla);
+    if (get_opt()) {
+        throw default_exception("setting preferred on optimization context is not supported yet");
+        return;
+    }
+}
+
+void cmd_context::reset_preferred() {
+    if (!m_scopes.empty())
+        throw default_exception("reset-preferred can only be invoked at base level");
+    if (m_preferred) 
+        m_preferred->reset_preferred();   
+}
+
 
 void cmd_context::display_model(model_ref& mdl) {
     if (mdl) {
@@ -2261,8 +2287,13 @@ void cmd_context::mk_solver() {
     m_params.get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled);
     m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic);
     m_solver = mk_slice_solver(m_solver.get());
-    if (m_simplifier_factory) 
+    if (m_simplifier_factory)
         m_solver = mk_simplifier_solver(m_solver.get(), &m_simplifier_factory);
+    if (m_preferred) {
+        auto p = m_preferred.get();
+        m_solver->user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh);
+        m_solver->user_propagate_register_decide(p->decide_eh);
+    }
 }
 
 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 83d0f06ee..ddc8b461a 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -39,6 +39,7 @@ Notes:
 #include "solver/check_logic.h"
 #include "solver/progress_callback.h"
 #include "solver/simplifier_solver.h"
+#include "solver/preferred_value_propagator.h"
 #include "cmd_context/pdecl.h"
 #include "cmd_context/tactic_manager.h"
 #include "params/context_params.h"
@@ -265,6 +266,7 @@ protected:
     dictionary<object_ref*>      m_object_refs; // anything that can be named.
     dictionary<sexpr*>           m_user_tactic_decls;
     vector<std::pair<expr_ref, expr_ref>> m_var2values;
+    scoped_ptr<preferred_value_propagator> m_preferred;
 
     dictionary<func_decls>       m_func_decls;
     obj_map<func_decl, symbol>   m_func_decl2alias;
@@ -429,6 +431,8 @@ public:
     void set_solver(solver* s) { m_solver = s; }
     void set_proof_cmds(proof_cmds* pc) { m_proof_cmds = pc; }
     void set_initial_value(expr* var, expr* value);
+    void set_preferred(expr *fmla);
+    void reset_preferred();
 
     void set_solver_factory(solver_factory * s);
     void set_simplifier_factory(simplifier_factory& sf) { m_simplifier_factory = sf; }
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 93f09f639..7b0afd7e1 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1890,6 +1890,8 @@ namespace smt {
 
     theory_bv::var_enode_pos theory_bv::get_bv_with_theory(bool_var v, theory_id id) const {
         atom* a      = get_bv2a(v);
+        if (!a)
+            return var_enode_pos(nullptr, UINT32_MAX);
         svector<var_enode_pos> vec;
         if (!a->is_bit())
             return var_enode_pos(nullptr, UINT32_MAX);
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index f8c2a35b8..d8adbdb70 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -209,61 +209,36 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
     if (!m_decide_eh)
         return;
 
-    const bool_var_data& d = ctx.get_bdata(var);
+    expr *e = ctx.bool_var2expr(var);
+    if (!e)
+        e = m.mk_true(); // use a dummy case split atom.
 
-    if (!d.is_enode() && !d.is_theory_atom())
-        return;
-
-    enode* original_enode = nullptr;
-    unsigned original_bit = 0;
-    bv_util bv(m);
-    theory* th = nullptr;
-    theory_var v = null_theory_var;
-
-    // get the associated theory
-    if (!d.is_enode()) {
-        // it might be a value that does not have an enode
-        th = ctx.get_theory(d.get_theory());
-    }
-    else {
-        original_enode = ctx.bool_var2enode(var);
-        v = original_enode->get_th_var(get_family_id());
-        if (v == null_theory_var) {
-            // it is not a registered boolean expression
-            th = ctx.get_theory(d.get_theory());
+    unsigned bit = 0;
+    // determine if case split is a bit-position in a bit-vector
+    {
+        bv_util bv(m);
+        auto th = ctx.get_theory(bv.get_fid());
+        if (th) {
+            // it is then n'th bit of a bit-vector n.
+            auto [n, nbit] = static_cast<theory_bv *>(th)->get_bv_with_theory(var, get_family_id());
+            if (n) {
+                e = n->get_expr();
+                bit = nbit;
+            }
         }
     }
 
-    if (v == null_theory_var && !th)
-        return;
-
-    if (v == null_theory_var && th->get_family_id() != bv.get_fid())
-        return;
-
-    if (v == null_theory_var) {
-        // it is not a registered boolean value but it is a bitvector
-        auto registered_bv = ((theory_bv*) th)->get_bv_with_theory(var, get_family_id());
-        if (!registered_bv.first)
-            // there is no registered bv associated with the bit
-            return;
-        original_enode = registered_bv.first;
-        original_bit = registered_bv.second;
-        v = original_enode->get_th_var(get_family_id());
-    }
-
-    // call the registered callback
-    unsigned new_bit = original_bit;
-
     force_push();
-    expr *e = var2expr(v);
-    m_decide_eh(m_user_context, this, e, new_bit, is_pos);
+    m_decide_eh(m_user_context, this, e, bit, is_pos);
 
     bool_var new_var;
     if (!get_case_split(new_var, is_pos) || new_var == var)
         // The user did not interfere
         return;
+    TRACE(user_propagate,
+          tout << "decide: " << ctx.bool_var2expr(var) << " -> " << ctx.bool_var2expr(new_var) << "\n");
     var = new_var;
-
+                    
     // check if the new variable is unassigned
     if (ctx.get_assignment(var) != l_undef)
         throw default_exception("expression in \"decide\" is already assigned");
diff --git a/src/solver/preferred_value_propagator.h b/src/solver/preferred_value_propagator.h
new file mode 100644
index 000000000..da83c1fa3
--- /dev/null
+++ b/src/solver/preferred_value_propagator.h
@@ -0,0 +1,85 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    preferred_value_propagator.h
+
+Abstract:
+
+    Specialized propagator for preferred values
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 10-2-2025
+
+Notes:
+
+--*/
+#pragma once
+
+#include "tactic/user_propagator_base.h"
+#include "util/trail.h"
+
+
+class preferred_value_propagator {
+    ast_manager &m;
+    expr_ref_vector m_preferred;
+    unsigned m_qhead = 0;
+    trail_stack m_trail;
+
+    bool decide(user_propagator::callback& cb) {
+        if (m_qhead >= m_preferred.size())
+            return false;
+        m_trail.push(value_trail(m_qhead));
+        while (m_qhead < m_preferred.size()) {
+            expr *e = m_preferred.get(m_qhead);
+            bool is_not = m.is_not(e, e);
+            m_qhead++;
+            if (cb.next_split_cb(e, 0, is_not ? l_false : l_true))
+                return true;
+        }
+        return false;
+    }
+
+public:
+    preferred_value_propagator(ast_manager &m) : m(m), m_preferred(m) {
+         push_eh = [](void * ctx, user_propagator::callback* cb) {
+            auto &p = *static_cast<preferred_value_propagator *>(ctx);
+            p.m_trail.push_scope(); 
+         };
+        pop_eh = [](void * ctx, user_propagator::callback* cb, unsigned n) -> void {
+            auto &p = *static_cast<preferred_value_propagator *>(ctx);
+            p.m_trail.pop_scope(n);
+        };
+        fresh_eh = [](void* ctx, ast_manager& dst, user_propagator::context_obj*& co) -> void* {
+            auto &p = *static_cast<preferred_value_propagator *>(ctx);
+            ast_translation tr(p.m, dst);
+            auto r = alloc(preferred_value_propagator, dst);
+            for (auto e : p.m_preferred)
+                r->set_preferred(tr(e));
+            return r;
+        };
+
+        decide_eh = [](void * ctx, user_propagator::callback * cb, expr *, unsigned, bool) -> bool {
+            auto &p = *static_cast<preferred_value_propagator *>(ctx);
+            return p.decide(*cb);
+        };
+    }
+    ~preferred_value_propagator() = default;
+    void set_preferred(expr *e) {
+        m_preferred.push_back(e);
+        if (m_trail.get_num_scopes() > 0)
+            m_trail.push(push_back_vector(m_preferred));
+    }
+    void reset_preferred() {
+        if (m_trail.get_num_scopes() != 0)
+            throw default_exception("cannot reset preferred values in scoped context");
+        m_preferred.reset();
+        SASSERT(m_qhead == 0);
+    }
+    user_propagator::push_eh_t push_eh;
+    user_propagator::pop_eh_t pop_eh;
+    user_propagator::fresh_eh_t fresh_eh;
+    user_propagator::decide_eh_t decide_eh;
+};
\ No newline at end of file