diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h
index 8f7680bc88..1957adb904 100644
--- a/src/V3AstNodeExpr.h
+++ b/src/V3AstNodeExpr.h
@@ -4678,6 +4678,7 @@ class AstSel final : public AstNodeTriop {
                : isWide()        ? "VL_SEL_%nq%lq%rq%tq(%nw,%lw, %P, %li, %ri, %ti)"
                                  : "VL_SEL_%nq%lq%rq%tq(%lw, %P, %li, %ri, %ti)";
     }
+    string emitSMT() const override { return "((_ extract %t %r) %l)"; }
     bool cleanOut() const override { return false; }
     bool cleanLhs() const override { return true; }
     bool cleanRhs() const override { return true; }
diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp
index e3fe9941d2..319eddfd85 100644
--- a/src/V3Randomize.cpp
+++ b/src/V3Randomize.cpp
@@ -529,6 +529,22 @@ class ConstraintExprVisitor final : public VNVisitor {
         if (editFormat(nodep)) return;
         editSMT(nodep, nodep->srcp());
     }
+    void visit(AstSel* nodep) override {
+        if (editFormat(nodep)) return;
+        VNRelinker handle;
+        AstNodeExpr* const widthp = nodep->widthp()->unlinkFrBack(&handle);
+        FileLine* const fl = nodep->fileline();
+        AstNodeExpr* const msbp
+            = new AstSFormatF{fl, "%1d", false,
+                              new AstAdd{fl, nodep->lsbp()->cloneTreePure(false),
+                                         new AstSub{fl, widthp, new AstConst{fl, 1}}}};
+        handle.relink(msbp);
+        AstNodeExpr* const lsbp
+            = new AstSFormatF{fl, "%1d", false, nodep->lsbp()->unlinkFrBack(&handle)};
+        handle.relink(lsbp);
+
+        editSMT(nodep, nodep->fromp(), lsbp, msbp);
+    }
     void visit(AstSFormatF* nodep) override {}
     void visit(AstStmtExpr* nodep) override {}
     void visit(AstConstraintIf* nodep) override {
diff --git a/test_regress/t/t_constraint_operators.v b/test_regress/t/t_constraint_operators.v
index c168e8af54..4dce0d3679 100644
--- a/test_regress/t/t_constraint_operators.v
+++ b/test_regress/t/t_constraint_operators.v
@@ -8,6 +8,7 @@ class Packet;
    rand int x;
    rand bit [31:0] b;
    rand bit [31:0] c;
+   rand bit [31:0] d;
    rand bit tiny;
    rand bit zero;
    rand bit one;
@@ -31,6 +32,7 @@ class Packet;
    constraint cond { (tiny == 1 ? b : c) != 17; }
    constraint zero_c { zero == 0; }
    constraint one_c { one == 1; }
+   constraint sel { d[15:8] == 8'h55; }
    constraint ifelse {
       if (one == 1) out0 == 'h333;
 
@@ -88,6 +90,7 @@ module t (/*AUTOARG*/);
       if (p.out4 != 'h333) $stop;
       if (p.out5 != 'h333) $stop;
       if (p.out6 != 'h333) $stop;
+      if (p.d[15:8] != 'h55) $stop;
 
       $write("*-* All Finished *-*\n");
       $finish;