diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 35a7894a8..961c717cf 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -263,6 +263,7 @@ namespace dd {
         inline PDD lo(PDD p) const { return m_nodes[p].m_lo; }
         inline PDD hi(PDD p) const { return m_nodes[p].m_hi; }
         inline rational const& val(PDD p) const { SASSERT(is_val(p)); return m_values[lo(p)]; }
+        inline rational const& val_signed(PDD p) const { SASSERT(m_semantics == mod2_e || m_semantics == mod2N_e); rational const& a = val(p); return a.get_bit(power_of_2() - 1) ? a - two_to_N() : a; }
         inline void inc_ref(PDD p) { if (m_nodes[p].m_refcount != max_rc) m_nodes[p].m_refcount++; SASSERT(!m_free_nodes.contains(p)); }
         inline void dec_ref(PDD p) { if (m_nodes[p].m_refcount != max_rc) m_nodes[p].m_refcount--; SASSERT(!m_free_nodes.contains(p)); }
         inline PDD level2pdd(unsigned l) const { return m_var2pdd[m_level2var[l]]; }
@@ -421,7 +422,8 @@ namespace dd {
         pdd hi() const { return pdd(m->hi(root), m); }
         unsigned index() const { return root; }
         unsigned var() const { return m->var(root); }
-        rational const& val() const { SASSERT(is_val()); return m->val(root); }
+        rational const& val() const { return m->val(root); }
+        rational const& val_signed() const { return m->val_signed(root); }
         rational const& leading_coefficient() const;
         rational const& offset() const { return m->offset(root); }
         bool is_val() const { return m->is_val(root); }
diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index 411ba5bd0..d3ebad245 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -614,28 +614,23 @@ namespace polysat {
         unsigned const p_sz = p.power_of_2();
         unsigned const q_sz = q.power_of_2();
         unsigned const v_sz = p_sz + q_sz;
-        if (p.is_val() && q.is_val()) {
-            rational const val = p.val() * rational::power_of_two(q_sz) + q.val();
-            return s.sz2pdd(v_sz).mk_val(val);
-        }
-        if (p.is_val()) {
-            // TODO
-        }
-        if (q.is_val()) {
-            // TODO
-        }
-        auto const args = {p, q};
-        return concat(args.size(), args.begin());
+        if (p.is_val() || q.is_val())
+            return zero_ext(p, q_sz) * rational::power_of_two(q_sz) + zero_ext(q, p_sz);
+        auto const args = {s.m_names.mk_name(p), s.m_names.mk_name(q)};
+        pvar const v = s.m_slicing.mk_concat(args.size(), args.begin());
+        return s.var(v);
     }
 
     pdd constraint_manager::concat(unsigned num_args, pdd const* args) {
         SASSERT(num_args > 0);
         if (num_args == 1)
             return args[0];
+        if (num_args == 2)
+            return concat(args[0], args[1]);
         // TODO: special cases when args are values?
         pvar_vector pvar_args;
         for (unsigned i = 0; i < num_args; ++i)
-            pvar_args.push_back(s.m_names.mk_name(args[i]));
+            pvar_args.push_back(s.m_names.mk_name_even_if_value(args[i]));
         pvar const v = s.m_slicing.mk_concat(num_args, pvar_args.data());
         return s.var(v);
     }
@@ -644,6 +639,8 @@ namespace polysat {
         SASSERT(extra_bits > 0);
         unsigned const p_sz = p.power_of_2();
         unsigned const v_sz = p_sz + extra_bits;
+        if (p.is_val())
+            return s.sz2pdd(v_sz).mk_val(p.val());
         pdd const q = s.var(s.m_names.mk_name(p));
         constraint_dedup::bv_ext_args const args = {false, q.var(), extra_bits};
         auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);
@@ -660,8 +657,10 @@ namespace polysat {
 
     pdd constraint_manager::sign_ext(pdd const& p, unsigned extra_bits) {
         SASSERT(extra_bits > 0);
-        unsigned const p_sz = p. power_of_2();
+        unsigned const p_sz = p.power_of_2();
         unsigned const v_sz = p_sz + extra_bits;
+        if (p.is_val())
+            return s.sz2pdd(v_sz).mk_val(p.val_signed());
         pdd const q = s.var(s.m_names.mk_name(p));
         constraint_dedup::bv_ext_args const args = {true, q.var(), extra_bits};
         auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);
diff --git a/src/math/polysat/naming.cpp b/src/math/polysat/naming.cpp
index 925dece54..df9ac6236 100644
--- a/src/math/polysat/naming.cpp
+++ b/src/math/polysat/naming.cpp
@@ -52,10 +52,10 @@ namespace polysat {
         return it->m_value;
     }
 
-    pvar name_manager::mk_name(pdd const& t) {
+    pvar name_manager::mk_name(pdd const& t, bool allow_values) {
         if (t.is_var())
             return t.var();
-        SASSERT(!t.is_val());  // we probably don't want names for constants
+        SASSERT(allow_values || !t.is_val());  // we probably don't want names for constants
         pvar v = get_name(t);
         if (v != null_var)
             return v;
diff --git a/src/math/polysat/naming.h b/src/math/polysat/naming.h
index 35cc4c38f..81bd8283c 100644
--- a/src/math/polysat/naming.h
+++ b/src/math/polysat/naming.h
@@ -45,6 +45,8 @@ namespace polysat {
 
         void set_name(pvar v, pdd const& term);
 
+        pvar mk_name(pdd const& term, bool allow_values);
+
     public:
         name_manager(solver& s): s(s) {}
 
@@ -53,13 +55,15 @@ namespace polysat {
 
         /** Whether v is a definition for a term */
         bool is_name(pvar v) const { return !m_terms[v].is_var() || m_terms[v].var() != v; }
+        pdd const& get_definition(pvar v) const { SASSERT(is_name(v)); return m_terms[v]; }
 
         /** Return name for term, or null_var if none has been created yet */
         pvar get_name(pdd const& term) const;
         bool has_name(pdd const& term) const { return get_name(term) != null_var; }
 
         /** Return name for term, creating one if necessary */
-        pvar mk_name(pdd const& term);
+        pvar mk_name(pdd const& term) { return mk_name(term, false); }
+        pvar mk_name_even_if_value(pdd const& term) { return mk_name(term, true); }
     };
 
 }