diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 38fa1e1d1..237cc5d11 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -3126,21 +3126,49 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
     }
     else if (re().is_range(r, r1, r2)) {
         expr_ref range(m());
-        expr_ref psi(m());
+        expr_ref psi(m().mk_false(), m());
         if (str().is_unit_string(r1, c1) && str().is_unit_string(r2, c2)) {
             SASSERT(u().is_char(c1));
             SASSERT(u().is_char(c2));
-            // range represents c1 <= e <= c2
+            // case: c1 <= e <= c2
             range = simplify_path(m().mk_and(u().mk_le(c1, e), u().mk_le(e, c2)));
             psi = simplify_path(m().mk_and(path, range));
-            if (m().is_false(psi))
-                result = nothing();
-            else
-                // D(e,c1..c2) = if (c1<=e<=c2) then () else []
-                result = re().mk_ite_simplify(range, epsilon(), nothing());
         }
-        else
+        else if (!str().is_string(r1) && str().is_unit_string(r2, c2)) {
+            SASSERT(u().is_char(c2));
+            // r1 nonground: |r1|=1 & r1[0] <= e <= c2
+            expr_ref one(m_autil.mk_int(1), m());
+            expr_ref zero(m_autil.mk_int(0), m());
+            expr_ref r1_length_eq_one(m().mk_eq(str().mk_length(r1), one), m());
+            expr_ref r1_0(str().mk_nth_i(r1, zero), m());
+            range = simplify_path(m().mk_and(r1_length_eq_one, m().mk_and(u().mk_le(r1_0, e), u().mk_le(e, c2))));
+            psi = simplify_path(m().mk_and(path, range));
+        }
+        else if (!str().is_string(r2) && str().is_unit_string(r1, c1)) {
+            SASSERT(u().is_char(c1));
+            // r2 nonground: |r2|=1 & c1 <= e <= r2_0
+            expr_ref one(m_autil.mk_int(1), m());
+            expr_ref zero(m_autil.mk_int(0), m());
+            expr_ref r2_length_eq_one(m().mk_eq(str().mk_length(r2), one), m());
+            expr_ref r2_0(str().mk_nth_i(r2, zero), m());
+            range = simplify_path(m().mk_and(r2_length_eq_one, m().mk_and(u().mk_le(c1, e), u().mk_le(e, r2_0))));
+            psi = simplify_path(m().mk_and(path, range));
+        }
+        else if (!str().is_string(r1) && !str().is_string(r2)) {
+            // both r1 and r2 nonground: |r1|=1 & |r2|=1 & r1[0] <= e <= r2[0]
+            expr_ref one(m_autil.mk_int(1), m());
+            expr_ref zero(m_autil.mk_int(0), m());
+            expr_ref r1_length_eq_one(m().mk_eq(str().mk_length(r1), one), m());
+            expr_ref r1_0(str().mk_nth_i(r1, zero), m());
+            expr_ref r2_length_eq_one(m().mk_eq(str().mk_length(r2), one), m());
+            expr_ref r2_0(str().mk_nth_i(r2, zero), m());
+            range = simplify_path(m().mk_and(r1_length_eq_one, m().mk_and(r2_length_eq_one, m().mk_and(u().mk_le(r1_0, e), u().mk_le(e, r2_0)))));
+            psi = simplify_path(m().mk_and(path, range));
+        }
+        if (m().is_false(psi))
             result = nothing();
+        else
+            result = re().mk_ite_simplify(range, epsilon(), nothing());
     }
     else if (re().is_union(r, r1, r2))
         result = mk_antimirov_deriv_union(mk_antimirov_deriv(e, r1, path), mk_antimirov_deriv(e, r2, path));
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 8f3001055..5245ea827 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -1233,11 +1233,11 @@ std::ostream& seq_util::rex::pp::print_unit(std::ostream& out, expr* s) const {
         print(out, e);
         out << "[" << mk_pp(i, re.m) << "]";
     }
-    else if (re.m.is_value(e))
-        out << mk_pp(e, re.m);
-    else if (is_app(e)) {
-        out << "(" << to_app(e)->get_decl()->get_name().str();
-        for (expr * arg : *to_app(e))
+    else if (re.m.is_value(s))
+        out << mk_pp(s, re.m);
+    else if (is_app(s)) {
+        out << "(" << to_app(s)->get_decl()->get_name().str();
+        for (expr * arg : *to_app(s))
             print(out << " ", arg);
         out << ")";
     }
@@ -1266,11 +1266,11 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
     else if (re.is_range(e, s, s2))
         print_range(out, s, s2);
     else if (re.is_epsilon(e))
-        // &#X03B5; = epsilon
-        out << (html_encode ? "&#X03B5;" : "()");
+        // &#x03B5; = epsilon
+        out << (html_encode ? "&#x03B5;" : "()");
     else if (re.is_empty(e))
-        // &#X2205; = emptyset
-        out << (html_encode ? "&#X2205;" : "[]");
+        // &#x2205; = emptyset
+        out << (html_encode ? "&#x2205;" : "[]");
     else if (re.is_concat(e, r1, r2)) {
         print(out, r1);
         print(out, r2);
@@ -1278,7 +1278,7 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
     else if (re.is_antimorov_union(e, r1, r2) || re.is_union(e, r1, r2)) {
         out << "(";
         print(out, r1);
-        out << (html_encode ? "&#X22C3;" : "|");
+        out << (html_encode ? "&#x22C3;" : "|");
         print(out, r2);
         out << ")";
     }
@@ -1286,7 +1286,7 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
     {
         out << "(";
         print(out, r1);
-        out << (html_encode ? "&#X22C2;" : "&");
+        out << (html_encode ? "&#x22C2;" : "&");
         print(out, r2);
         out << ")";
     }
@@ -1359,11 +1359,11 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
         out << ")";
     }
     else if (re.m.is_ite(e, s, r1, r2)) {
-        out << (html_encode ? "(&#X1D422;&#X1D41F; " : "(if ");
+        out << (html_encode ? "(&#x1D422;&#x1D41F; " : "(if ");
         print(out, s);
-        out << (html_encode ? " &#X1D42D;&#X1D5F5;&#X1D41E;&#X1D427; " : " then ");
+        out << (html_encode ? " &#x1D42D;&#x1D5F5;&#x1D41E;&#x1D427; " : " then ");
         print(out, r1);
-        out << (html_encode ? " &#X1D41E;&#X1D425;&#X1D600;&#X1D41E; " : " else ");
+        out << (html_encode ? " &#x1D41E;&#x1D425;&#x1D600;&#x1D41E; " : " else ");
         print(out, r2);
         out << ")";
     }