diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp
index e5aadf836..b7b162add 100644
--- a/src/V3Assert.cpp
+++ b/src/V3Assert.cpp
@@ -142,6 +142,7 @@ class AssertVisitor final : public VNVisitor {
     VDouble0 m_statAsFull;  // Statistic tracking
     VDouble0 m_statPastVars;  // Statistic tracking
     bool m_inSampled = false;  // True inside a sampled expression
+    bool m_inRestrict = false;  // True inside restrict assertion
 
     // METHODS
     static AstNodeExpr* assertOnCond(FileLine* fl, VAssertType type,
@@ -274,6 +275,38 @@ class AssertVisitor final : public VNVisitor {
         return newp;
     }
 
+    static AstIf* assertCond(AstNodeCoverOrAssert* nodep, AstNodeExpr* propp, AstNode* passsp,
+                             AstNode* failsp) {
+
+        AstIf* const ifp = new AstIf{nodep->fileline(), propp, passsp, failsp};
+        // It's more LIKELY that we'll take the nullptr if clause
+        // than the sim-killing else clause:
+        ifp->branchPred(VBranchPred::BP_LIKELY);
+        ifp->isBoundsCheck(true);  // To avoid LATCH warning
+        return ifp;
+    }
+
+    static AstNode* assertBody(AstNodeCoverOrAssert* nodep, AstNodeExpr* propp, AstNode* passsp,
+                               AstNode* failsp) {
+        if (AstPExpr* const pExpr = VN_CAST(propp, PExpr)) {
+            AstNodeExpr* const condp = pExpr->condp();
+            UASSERT_OBJ(condp, pExpr, "Should have condition");
+            AstIf* const ifp = assertCond(nodep, condp->unlinkFrBack(), passsp, failsp);
+
+            AstNode* const precondps = pExpr->precondp();
+            UASSERT_OBJ(precondps, pExpr, "Should have precondition");
+            precondps->unlinkFrBackWithNext()->addNext(ifp);
+            AstNodeStmt* const assertOnp
+                = newIfAssertOn(precondps, nodep->directive(), nodep->type());
+            AstFork* const forkp = new AstFork{precondps->fileline(), "", assertOnp};
+            forkp->joinType(VJoinType::JOIN_NONE);
+            return forkp;
+        }
+
+        AstIf* const ifp = assertCond(nodep, propp, passsp, failsp);
+        return newIfAssertOn(ifp, nodep->directive(), nodep->type());
+    }
+
     AstNodeStmt* newFireAssertUnchecked(const AstNodeStmt* nodep, const string& message,
                                         AstNodeExpr* exprsp = nullptr) {
         // Like newFireAssert() but omits the asserts-on check
@@ -321,9 +354,7 @@ class AssertVisitor final : public VNVisitor {
             }
         }
         //
-        AstNode* bodysp = nullptr;
         bool selfDestruct = false;
-        AstIf* ifp = nullptr;
         if (const AstCover* const snodep = VN_CAST(nodep, Cover)) {
             ++m_statCover;
             if (!v3Global.opt.coverageUser()) {
@@ -334,14 +365,12 @@ class AssertVisitor final : public VNVisitor {
                 UASSERT_OBJ(covincp, snodep, "Missing AstCoverInc under assertion");
                 covincp->unlinkFrBackWithNext();  // next() might have  AstAssign for trace
                 if (message != "") covincp->declp()->comment(message);
-                bodysp = covincp;
+                if (passsp) {
+                    passsp = AstNode::addNext<AstNode, AstNode>(covincp, passsp);
+                } else {
+                    passsp = covincp;
+                }
             }
-
-            if (bodysp && passsp) bodysp = bodysp->addNext(passsp);
-            if (bodysp) bodysp = newIfAssertOn(bodysp, nodep->directive(), nodep->type());
-            ifp = new AstIf{nodep->fileline(), propp, bodysp};
-            ifp->isBoundsCheck(true);  // To avoid LATCH warning
-            bodysp = ifp;
         } else if (VN_IS(nodep, Assert) || VN_IS(nodep, AssertIntrinsic)) {
             if (nodep->immediate()) {
                 ++m_statAsImm;
@@ -349,33 +378,26 @@ class AssertVisitor final : public VNVisitor {
                 ++m_statAsNotImm;
             }
             if (!passsp && !failsp) failsp = newFireAssertUnchecked(nodep, "'assert' failed.");
-            ifp = new AstIf{nodep->fileline(), propp, passsp, failsp};
-            ifp->isBoundsCheck(true);  // To avoid LATCH warning
-            // It's more LIKELY that we'll take the nullptr if clause
-            // than the sim-killing else clause:
-            ifp->branchPred(VBranchPred::BP_LIKELY);
-            bodysp = newIfAssertOn(ifp, nodep->directive(), nodep->type());
         } else {
             nodep->v3fatalSrc("Unknown node type");
         }
 
+        AstNode* bodysp = assertBody(nodep, propp, passsp, failsp);
+        if (sentreep) {
+            bodysp = new AstAlways{nodep->fileline(), VAlwaysKwd::ALWAYS, sentreep, bodysp};
+        }
+
         if (passsp && !passsp->backp()) VL_DO_DANGLING(pushDeletep(passsp), passsp);
         if (failsp && !failsp->backp()) VL_DO_DANGLING(pushDeletep(failsp), failsp);
 
-        AstNode* newp;
-        if (sentreep) {
-            newp = new AstAlways{nodep->fileline(), VAlwaysKwd::ALWAYS, sentreep, bodysp};
-        } else {
-            newp = bodysp;
-        }
         // Install it
         if (selfDestruct) {
             // Delete it after making the tree.  This way we can tell the user
             // if it wasn't constructed nicely or has other errors without needing --coverage.
-            VL_DO_DANGLING(newp->deleteTree(), newp);
+            VL_DO_DANGLING(bodysp->deleteTree(), bodysp);
             nodep->unlinkFrBack();
         } else {
-            nodep->replaceWith(newp);
+            nodep->replaceWith(bodysp);
         }
         // Bye
         VL_DO_DANGLING(pushDeletep(nodep), nodep);
@@ -579,6 +601,7 @@ class AssertVisitor final : public VNVisitor {
             AstVar* const outvarp = new AstVar{
                 nodep->fileline(), VVarType::MODULETEMP,
                 "_Vpast_" + cvtToStr(m_modPastNum++) + "_" + cvtToStr(i), inp->dtypep()};
+            outvarp->lifetime(VLifetime::AUTOMATIC_EXPLICIT);
             ++m_statPastVars;
             m_modp->addStmtsp(outvarp);
             AstNode* const assp = new AstAssignDly{
@@ -605,7 +628,7 @@ class AssertVisitor final : public VNVisitor {
     }
     void visit(AstVarRef* nodep) override {
         iterateChildren(nodep);
-        if (m_inSampled) {
+        if (m_inSampled && !VString::startsWith(nodep->name(), "__VpropPrecond")) {
             if (!nodep->access().isReadOnly()) {
                 nodep->v3warn(E_UNSUPPORTED,
                               "Unsupported: Write to variable in sampled expression");
@@ -625,6 +648,19 @@ class AssertVisitor final : public VNVisitor {
         m_inSampled = false;
         iterateChildren(nodep);
     }
+    void visit(AstPExpr* nodep) override {
+        {
+            VL_RESTORER(m_inSampled);
+            m_inSampled = false;
+            iterateAndNextNull(nodep->precondp());
+        }
+        iterate(nodep->condp());
+        if (!m_inRestrict) {
+            VL_DO_DANGLING(pushDeletep(nodep), nodep);
+        } else {
+            VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
+        }
+    }
 
     //========== Statements
     void visit(AstDisplay* nodep) override {
@@ -790,6 +826,8 @@ class AssertVisitor final : public VNVisitor {
         visitAssertionIterate(nodep, nullptr);
     }
     void visit(AstRestrict* nodep) override {
+        VL_RESTORER(m_inRestrict);
+        m_inRestrict = true;
         iterateChildren(nodep);
         // IEEE says simulator ignores these
         VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp
index b31b2da0d..2db7d53b4 100644
--- a/src/V3AssertPre.cpp
+++ b/src/V3AssertPre.cpp
@@ -56,10 +56,15 @@ private:
     AstNodeExpr* m_disablep = nullptr;  // Last disable
     // Other:
     V3UniqueNames m_cycleDlyNames{"__VcycleDly"};  // Cycle delay counter name generator
+    V3UniqueNames m_propPrecondNames{"__VpropPrecond"};  // Cycle delay temporaries name generator
     bool m_inAssign = false;  // True if in an AssignNode
     bool m_inAssignDlyLhs = false;  // True if in AssignDly's LHS
     bool m_inSynchDrive = false;  // True if in synchronous drive
     std::vector<AstVarXRef*> m_xrefsp;  // list of xrefs that need name fixup
+    AstNodeExpr* m_hasUnsupp = nullptr;  // True if assert has unsupported construct inside
+    AstPExpr* m_pExpr = nullptr;  // Current AstPExpr
+    bool m_hasSExpr = false;  // True if assert has AstSExpr inside
+    bool m_inSExpr = false;  // True if in AstSExpr
 
     // METHODS
 
@@ -335,16 +340,21 @@ private:
             VL_DO_DANGLING(valuep->deleteTree(), valuep);
             return;
         }
+        AstSenItem* sensesp = nullptr;
         if (!m_defaultClockingp) {
-            nodep->v3error("Usage of cycle delays requires default clocking"
-                           " (IEEE 1800-2023 14.11)");
-            VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
-            VL_DO_DANGLING(valuep->deleteTree(), valuep);
-            return;
+            if (!m_pExpr && !m_inSExpr) {
+                nodep->v3error("Usage of cycle delays requires default clocking"
+                               " (IEEE 1800-2023 14.11)");
+                VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
+                VL_DO_DANGLING(valuep->deleteTree(), valuep);
+                return;
+            }
+            sensesp = m_senip;
+        } else {
+            sensesp = m_defaultClockingp->sensesp();
         }
         AstEventControl* const controlp = new AstEventControl{
-            nodep->fileline(),
-            new AstSenTree{flp, m_defaultClockingp->sensesp()->cloneTree(false)}, nullptr};
+            nodep->fileline(), new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr};
         const std::string delayName = m_cycleDlyNames.get(nodep);
         AstVar* const cntVarp = new AstVar{flp, VVarType::BLOCKTEMP, delayName + "__counter",
                                            nodep->findBasicDType(VBasicDTypeKwd::UINT32)};
@@ -408,6 +418,33 @@ private:
                 }
             }
             nodep->user1(true);
+        } else if (m_inSExpr && !nodep->user1()) {
+            AstVar* const preVarp
+                = new AstVar{nodep->varp()->fileline(), VVarType::BLOCKTEMP,
+                             m_propPrecondNames.get(nodep->varp()) + "__" + nodep->varp()->name(),
+                             nodep->varp()->dtypep()};
+            preVarp->lifetime(VLifetime::STATIC_EXPLICIT);
+            m_modp->addStmtsp(preVarp);
+            AstVarRef* const origp
+                = new AstVarRef{nodep->fileline(), nodep->varp(), VAccess::READ};
+            origp->user1(true);
+            AstVarRef* const precondp
+                = new AstVarRef{preVarp->fileline(), preVarp, VAccess::WRITE};
+            precondp->user1(true);
+
+            // Pack assignments in sampled as in concurrent assertions they are needed.
+            // Then, in assert's propp, sample only non-precondition variables.
+            AstSampled* const sampledp = new AstSampled{origp->fileline(), origp};
+            sampledp->dtypeFrom(origp);
+            UASSERT(m_pExpr, "Should be under assertion");
+            AstAssign* const assignp = new AstAssign{m_pExpr->fileline(), precondp, sampledp};
+            m_pExpr->addPrecondp(assignp);
+
+            AstVarRef* const precondReadp
+                = new AstVarRef{preVarp->fileline(), preVarp, VAccess::READ};
+            precondReadp->user1(true);
+            nodep->replaceWith(precondReadp);
+            VL_DO_DANGLING(pushDeletep(nodep), nodep);
         }
     }
     void visit(AstMemberSel* nodep) override {
@@ -461,10 +498,33 @@ private:
 
     void visit(AstNodeCoverOrAssert* nodep) override {
         if (nodep->sentreep()) return;  // Already processed
+
+        VL_RESTORER(m_hasSExpr);
+        VL_RESTORER(m_hasUnsupp);
+
         clearAssertInfo();
+        m_pExpr = new AstPExpr{nodep->propp()->fileline()};
+        m_pExpr->dtypeFrom(nodep->propp());
+
         // Find Clocking's buried under nodep->exprsp
         iterateChildren(nodep);
         if (!nodep->immediate()) nodep->sentreep(newSenTree(nodep));
+        if (m_hasSExpr && m_hasUnsupp) {
+            if (VN_IS(m_hasUnsupp, Implication)) {
+                m_hasUnsupp->v3warn(E_UNSUPPORTED,
+                                    "Unsupported: Implication with sequence expression");
+            } else {
+                m_hasUnsupp->v3warn(E_UNSUPPORTED,
+                                    "Unsupported: Disable iff with sequence expression");
+            }
+            if (m_pExpr) VL_DO_DANGLING(pushDeletep(m_pExpr), m_pExpr);
+        } else if (m_pExpr && m_pExpr->precondp()) {
+            m_pExpr->condp(VN_AS(nodep->propp()->unlinkFrBackWithNext(), NodeExpr));
+            nodep->propp(m_pExpr);
+            iterateAndNextNull(m_pExpr->precondp());
+        } else if (m_pExpr) {
+            VL_DO_DANGLING(pushDeletep(m_pExpr), m_pExpr);
+        }
         clearAssertInfo();
     }
     void visit(AstFalling* nodep) override {
@@ -488,12 +548,12 @@ private:
         if (exprp->width() > 1) exprp = new AstSel{fl, exprp, 0, 1};
         AstSenTree* sentreep = nodep->sentreep();
         if (sentreep) sentreep->unlinkFrBack();
-        AstNodeExpr* const pastp = new AstPast{fl, exprp};
+        AstPast* const pastp = new AstPast{fl, exprp};
         pastp->dtypeFrom(exprp);
+        pastp->sentreep(newSenTree(nodep, sentreep));
         exprp = new AstAnd{fl, pastp, new AstNot{fl, exprp->cloneTreePure(false)}};
         exprp->dtypeSetBit();
         nodep->replaceWith(exprp);
-        nodep->sentreep(newSenTree(nodep, sentreep));
         VL_DO_DANGLING(pushDeletep(nodep), nodep);
     }
     void visit(AstFuture* nodep) override {
@@ -503,6 +563,10 @@ private:
         if (sentreep) VL_DO_DANGLING(pushDeletep(sentreep->unlinkFrBack()), sentreep);
         nodep->sentreep(newSenTree(nodep));
     }
+    void visit(AstLogNot* nodep) override {
+        if (m_inSExpr) nodep->v3error("Syntax error: unexpected 'not' in sequence expression");
+        iterateChildren(nodep);
+    }
     void visit(AstPast* nodep) override {
         if (nodep->sentreep()) return;  // Already processed
         iterateChildren(nodep);
@@ -529,12 +593,12 @@ private:
         if (exprp->width() > 1) exprp = new AstSel{fl, exprp, 0, 1};
         AstSenTree* sentreep = nodep->sentreep();
         if (sentreep) sentreep->unlinkFrBack();
-        AstNodeExpr* const pastp = new AstPast{fl, exprp};
+        AstPast* const pastp = new AstPast{fl, exprp};
         pastp->dtypeFrom(exprp);
+        pastp->sentreep(newSenTree(nodep, sentreep));
         exprp = new AstAnd{fl, new AstNot{fl, pastp}, exprp->cloneTreePure(false)};
         exprp->dtypeSetBit();
         nodep->replaceWith(exprp);
-        nodep->sentreep(newSenTree(nodep, sentreep));
         VL_DO_DANGLING(pushDeletep(nodep), nodep);
     }
     void visit(AstStable* nodep) override {
@@ -544,12 +608,12 @@ private:
         AstNodeExpr* exprp = nodep->exprp()->unlinkFrBack();
         AstSenTree* sentreep = nodep->sentreep();
         if (sentreep) sentreep->unlinkFrBack();
-        AstNodeExpr* const pastp = new AstPast{fl, exprp};
+        AstPast* const pastp = new AstPast{fl, exprp};
         pastp->dtypeFrom(exprp);
+        pastp->sentreep(newSenTree(nodep, sentreep));
         exprp = new AstEq{fl, pastp, exprp->cloneTreePure(false)};
         exprp->dtypeSetBit();
         nodep->replaceWith(exprp);
-        nodep->sentreep(newSenTree(nodep, sentreep));
         VL_DO_DANGLING(pushDeletep(nodep), nodep);
     }
     void visit(AstSteady* nodep) override {
@@ -568,21 +632,27 @@ private:
 
     void visit(AstImplication* nodep) override {
         if (nodep->sentreep()) return;  // Already processed
+        m_hasUnsupp = nodep;
 
-        FileLine* const fl = nodep->fileline();
+        iterateChildren(nodep);
+
+        FileLine* const flp = nodep->fileline();
         AstNodeExpr* const rhsp = nodep->rhsp()->unlinkFrBack();
         AstNodeExpr* lhsp = nodep->lhsp()->unlinkFrBack();
+        if (nodep->isOverlapped()) {
+            nodep->replaceWith(new AstLogOr{flp, new AstLogNot{flp, lhsp}, rhsp});
+        } else {
+            if (m_disablep) {
+                lhsp = new AstAnd{flp, new AstNot{flp, m_disablep->cloneTreePure(false)}, lhsp};
+            }
 
-        if (m_disablep) {
-            lhsp = new AstAnd{fl, new AstNot{fl, m_disablep->cloneTreePure(false)}, lhsp};
+            AstPast* const pastp = new AstPast{flp, lhsp};
+            pastp->dtypeFrom(lhsp);
+            pastp->sentreep(newSenTree(nodep));
+            AstNodeExpr* const exprp = new AstOr{flp, new AstNot{flp, pastp}, rhsp};
+            exprp->dtypeSetBit();
+            nodep->replaceWith(exprp);
         }
-
-        AstNodeExpr* const pastp = new AstPast{fl, lhsp};
-        pastp->dtypeFrom(lhsp);
-        AstNodeExpr* const exprp = new AstOr{fl, new AstNot{fl, pastp}, rhsp};
-        exprp->dtypeSetBit();
-        nodep->replaceWith(exprp);
-        nodep->sentreep(newSenTree(nodep));
         VL_DO_DANGLING(pushDeletep(nodep), nodep);
     }
 
@@ -614,6 +684,7 @@ private:
         }
         if (AstNodeExpr* const disablep = nodep->disablep()) {
             m_disablep = disablep;
+            m_hasUnsupp = disablep;
             if (VN_IS(nodep->backp(), Cover)) {
                 blockp = new AstAnd{disablep->fileline(),
                                     new AstNot{disablep->fileline(), disablep->unlinkFrBack()},
@@ -627,6 +698,18 @@ private:
         nodep->replaceWith(blockp);
         VL_DO_DANGLING(pushDeletep(nodep), nodep);
     }
+    void visit(AstSExpr* nodep) override {
+        VL_RESTORER(m_inSExpr);
+        m_inSExpr = true;
+        m_hasSExpr = true;
+
+        UASSERT_OBJ(m_pExpr, nodep, "Should be under assertion");
+        m_pExpr->addPrecondp(nodep->delayp()->unlinkFrBack());
+
+        iterateChildren(nodep);
+        nodep->replaceWith(nodep->exprp()->unlinkFrBack());
+        VL_DO_DANGLING(pushDeletep(nodep), nodep);
+    }
     void visit(AstNodeModule* nodep) override {
         VL_RESTORER(m_defaultClockingp);
         VL_RESTORER(m_defaultDisablep);
diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h
index 2538c79c6..8014553d1 100644
--- a/src/V3AstNodeExpr.h
+++ b/src/V3AstNodeExpr.h
@@ -1523,14 +1523,19 @@ public:
 };
 class AstImplication final : public AstNodeExpr {
     // Verilog Implication Operator
-    // Nonoverlapping "|=>"
-    // Overlapping "|->" (doesn't currently use this - might make new Ast type)
+    // Nonoverlapped "|=>"
+    // Overlapped "|->"
     // @astgen op1 := lhsp : AstNodeExpr
     // @astgen op2 := rhsp : AstNodeExpr
     // @astgen op3 := sentreep : Optional[AstSenTree]
+
+private:
+    const bool m_isOverlapped;  // True if overlapped
+
 public:
-    AstImplication(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp)
-        : ASTGEN_SUPER_Implication(fl) {
+    AstImplication(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp, bool isOverlapped)
+        : ASTGEN_SUPER_Implication(fl)
+        , m_isOverlapped{isOverlapped} {
         this->lhsp(lhsp);
         this->rhsp(rhsp);
     }
@@ -1541,6 +1546,7 @@ public:
     bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
     int instrCount() const override { return widthInstrs(); }
     bool sameNode(const AstNode* /*samep*/) const override { return true; }
+    bool isOverlapped() const { return m_isOverlapped; }
 };
 class AstInitArray final : public AstNodeExpr {
     // This is also used as an array value in V3Simulate/const prop.
@@ -1706,6 +1712,19 @@ public:
     bool sameNode(const AstNode* /*samep*/) const override { return true; }
     int instrCount() const override { return widthInstrs(); }
 };
+class AstPExpr final : public AstNodeExpr {
+    // Property expression
+    // @astgen op1 := precondp : List[AstNode]
+    // @astgen op2 := condp : Optional[AstNodeExpr]
+public:
+    explicit AstPExpr(FileLine* fl)
+        : ASTGEN_SUPER_PExpr(fl) {}
+    ASTGEN_MEMBERS_AstPExpr;
+    string emitVerilog() override { V3ERROR_NA_RETURN(""); }
+    string emitC() override { V3ERROR_NA_RETURN(""); }
+    bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
+    int instrCount() const override { return widthInstrs(); }
+};
 class AstParseHolder final : public AstNodeExpr {
     // A reference to something soon to replace, used in a select at parse time
     // that needs conversion to pull the upper lvalue later
@@ -1915,6 +1934,22 @@ public:
     int instrCount() const override { return widthInstrs(); }
     bool sameNode(const AstNode* /*samep*/) const override { return true; }
 };
+class AstSExpr final : public AstNodeExpr {
+    // Sequence expression
+    // @astgen op1 := delayp : AstDelay
+    // @astgen op2 := exprp : AstNodeExpr
+public:
+    explicit AstSExpr(FileLine* fl, AstDelay* delayp, AstNodeExpr* exprp)
+        : ASTGEN_SUPER_SExpr(fl) {
+        this->delayp(delayp);
+        this->exprp(exprp);
+    }
+    ASTGEN_MEMBERS_AstSExpr;
+    string emitVerilog() override { V3ERROR_NA_RETURN(""); }
+    string emitC() override { V3ERROR_NA_RETURN(""); }
+    bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
+    int instrCount() const override { return widthInstrs(); }
+};
 class AstSFormatF final : public AstNodeExpr {
     // Convert format to string, generally under an AstDisplay or AstSFormat
     // Also used as "real" function for /*verilator sformat*/ functions
diff --git a/src/V3AstNodeStmt.h b/src/V3AstNodeStmt.h
index 7b4d549dd..c934fd290 100644
--- a/src/V3AstNodeStmt.h
+++ b/src/V3AstNodeStmt.h
@@ -1204,6 +1204,9 @@ public:
         : ASTGEN_SUPER_Assert(fl, propp, passsp, type, directive, name) {
         addFailsp(failsp);
     }
+    string verilogKwd() const override {
+        return directive() == VAssertDirectiveType::ASSERT ? "assert" : "assume";
+    }
 };
 class AstAssertIntrinsic final : public AstNodeCoverOrAssert {
     // A $cast or other compiler inserted assert, that must run even without --assert option
@@ -1217,6 +1220,7 @@ public:
                                        VAssertDirectiveType::INTRINSIC, name) {
         addFailsp(failsp);
     }
+    string verilogKwd() const override { return "assert"; }
 };
 class AstCover final : public AstNodeCoverOrAssert {
     // @astgen op3 := coverincsp: List[AstNode] // Coverage node
@@ -1225,6 +1229,7 @@ public:
     AstCover(FileLine* fl, AstNode* propp, AstNode* stmtsp, VAssertType type,
              const string& name = "")
         : ASTGEN_SUPER_Cover(fl, propp, stmtsp, type, VAssertDirectiveType::COVER, name) {}
+    string verilogKwd() const override { return "cover"; }
 };
 class AstRestrict final : public AstNodeCoverOrAssert {
 public:
@@ -1233,6 +1238,7 @@ public:
         // Intrinsic asserts are always ignored thus 'type' field is set to INTERNAL.
         : ASTGEN_SUPER_Restrict(fl, propp, nullptr, VAssertType::INTERNAL,
                                 VAssertDirectiveType::RESTRICT) {}
+    string verilogKwd() const override { return "restrict"; }
 };
 
 // === AstNodeForeach ===
diff --git a/src/V3EmitV.cpp b/src/V3EmitV.cpp
index 617feeb96..9b6f052a6 100644
--- a/src/V3EmitV.cpp
+++ b/src/V3EmitV.cpp
@@ -37,7 +37,9 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
     AstSenTree* m_sentreep = nullptr;  // Domain for printing one a ALWAYS under a ACTIVE
     bool m_suppressSemi = false;  // Non-statement, don't print ;
     bool m_suppressVarSemi = false;  // Suppress emitting semicolon for AstVars
+    bool m_suppressSampled = false;  // Suppress emitting sampled in assertion properties
     bool m_arrayPost = false;  // Print array information that goes after identifier (vs after)
+    bool m_prefixed = true;  // Whether constants need to be prefixed
     std::deque<AstNodeArrayDType*> m_packedps;  // Packed arrays to print with BasicDType
     std::unordered_map<AstJumpBlock*, size_t> m_labelNumbers;  // Label numbers for JumpBlocks
 
@@ -79,14 +81,13 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
     }
     void visit(AstPort* nodep) override {}
     void visit(AstNodeFTask* nodep) override {
-        const bool func = nodep->isFunction() || nodep->name() == "new";
-        putfs(nodep, func ? "function" : "task");
+        putfs(nodep, nodep->verilogKwd());
         puts(" ");
         puts(nodep->prettyName());
         puts(";\n");
         // Only putfs the first time for each visitor; later for same node is putqs
         iterateAndNextConstNull(nodep->stmtsp());
-        putfs(nodep, func ? "endfunction\n" : "endtask\n");
+        putqs(nodep, "end" + nodep->verilogKwd() + "\n");
     }
 
     void visit(AstGenBlock* nodep) override {
@@ -466,9 +467,11 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
         puts(")");
     }
     void visit(AstSampled* nodep) override {
-        putfs(nodep, "$sampled(");
-        iterateAndNextConstNull(nodep->exprp());
-        puts(")");
+        if (!m_suppressSampled) {
+            putfs(nodep, "$sampled(");
+            iterateAndNextConstNull(nodep->exprp());
+            puts(")");
+        }
     }
     void visit(AstRising* nodep) override {
         putfs(nodep, "$rising(");
@@ -757,6 +760,47 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
         puts(nodep->prettyName());
         puts(";\n");
     }
+    void visit(AstNodeCoverOrAssert* nodep) override {
+        if (AstPExpr* const pexprp = VN_CAST(nodep->propp(), PExpr)) {
+            iterateAndNextConstNull(pexprp);
+        }
+        putfs(nodep, nodep->verilogKwd() + " ");
+        if (nodep->type() == VAssertType::OBSERVED_DEFERRED_IMMEDIATE) {
+            puts("#0 ");
+        } else if (nodep->type() == VAssertType::FINAL_DEFERRED_IMMEDIATE) {
+            puts("final ");
+        } else if (nodep->type() == VAssertType::CONCURRENT) {
+            puts("property ");
+        }
+        iterateConstNull(nodep->sentreep());
+        puts("(");
+        if (const AstPExpr* const pexprp = VN_CAST(nodep->propp(), PExpr)) {
+            iterateAndNextConstNull(pexprp->condp());
+        } else {
+            if (AstSampled* const sampledp = VN_CAST(nodep->propp(), Sampled)) {
+                iterateAndNextConstNull(sampledp->exprp());
+            } else {
+                iterateAndNextConstNull(nodep->propp());
+            }
+        }
+        if (!VN_IS(nodep, Restrict)) {
+            puts(") begin\n");
+            iterateAndNextConstNull(nodep->passsp());
+            puts("end\n");
+        } else {
+            puts(");\n");
+        }
+
+        if (const AstAssert* const assertp = VN_CAST(nodep, Assert)) {
+            puts("else begin\n");
+            iterateAndNextConstNull(assertp->failsp());
+            puts("end\n");
+        } else if (const AstAssertIntrinsic* const assertp = VN_CAST(nodep, AssertIntrinsic)) {
+            puts("else begin\n");
+            iterateAndNextConstNull(assertp->failsp());
+            puts("end\n");
+        }
+    }
     void visit(AstAssocArrayDType* nodep) override {
         if (!m_arrayPost) {
             iterateConst(nodep->subDTypep());
@@ -934,9 +978,11 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
         } else {
             putfs(nodep, nodep->prettyName());
         }
-        puts("(");
-        iterateAndNextConstNull(nodep->pinsp());
-        puts(")");
+        if (!VN_IS(nodep->taskp(), Property)) {
+            puts("(");
+            iterateAndNextConstNull(nodep->pinsp());
+            puts(")");
+        }
     }
     void visit(AstCCall* nodep) override {
         puts(nodep->funcp()->name());
@@ -949,6 +995,36 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
         puts(nodep->verilogKwd());
         puts(";\n");
     }
+    void visit(AstPropSpec* nodep) override {
+        if (!VN_IS(nodep->propp(), FuncRef)) {
+            // Same dumping as in AstSenTree
+            putfs(nodep, "@(");
+            for (AstNode* expp = nodep->sensesp(); expp; expp = expp->nextp()) {
+                iterateConst(expp);
+                if (expp->nextp()) putqs(expp->nextp(), " or ");
+            }
+            puts(")");
+        }
+        if (nodep->disablep()) {
+            puts(" disable iff ");
+            iterateConst(nodep->disablep());
+        }
+
+        puts(" ");
+        iterateConstNull(nodep->propp());
+        puts("\n");
+    }
+    void visit(AstPExpr* nodep) override {
+        iterateAndNextConstNull(nodep->precondp());  // condp emitted by AstNodeCoverOrAssert
+    }
+    void visit(AstSExpr* nodep) override {
+        {
+            VL_RESTORER(m_suppressSemi);
+            m_suppressSemi = true;
+            iterateConstNull(nodep->delayp());
+        }
+        iterateConstNull(nodep->exprp());
+    }
 
     // Terminals
     void visit(AstVarRef* nodep) override {
@@ -977,7 +1053,7 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
             puts(nodep->prettyName());
         }
     }
-    void visit(AstConst* nodep) override { putfs(nodep, nodep->num().ascii(true, true)); }
+    void visit(AstConst* nodep) override { putfs(nodep, nodep->num().ascii(m_prefixed, true)); }
 
     // Just iterate
     void visit(AstTopScope* nodep) override { iterateChildrenConst(nodep); }
@@ -1003,9 +1079,19 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
     }
     void visit(AstDelay* nodep) override {
         puts("");  // this is for proper alignment
-        puts("#");
+        if (nodep->isCycleDelay()) {
+            puts("##");
+        } else {
+            puts("#");
+        }
+        VL_RESTORER(m_prefixed);
+        m_prefixed = false;
         iterateConst(nodep->lhsp());
-        puts(";\n");
+        if (!m_suppressSemi) {
+            puts(";\n");
+        } else {
+            puts(" ");
+        }
         iterateAndNextConstNull(nodep->stmtsp());
     }
     void visit(AstCAwait* nodep) override {
diff --git a/src/V3Width.cpp b/src/V3Width.cpp
index eafd432dc..87c0e000c 100644
--- a/src/V3Width.cpp
+++ b/src/V3Width.cpp
@@ -1551,6 +1551,13 @@ class WidthVisitor final : public VNVisitor {
             if (nodep->seedp()) iterateCheckSigned32(nodep, "seed", nodep->seedp(), BOTH);
         }
     }
+    void visit(AstSExpr* nodep) override {
+        if (m_vup->prelim()) {
+            iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH);
+            iterate(nodep->delayp());
+            nodep->dtypeSetBit();
+        }
+    }
     void visit(AstURandomRange* nodep) override {
         if (m_vup->prelim()) {
             nodep->dtypeSetUInt32();  // Says the spec
diff --git a/src/verilog.y b/src/verilog.y
index 1abe0b82c..ffc3ff35e 100644
--- a/src/verilog.y
+++ b/src/verilog.y
@@ -6519,8 +6519,8 @@ pexpr<nodeExprp>:  // IEEE: property_expr  (The name pexpr is important as regex
         //
         //                      // IEEE: "sequence_expr yP_ORMINUSGT pexpr"
         //                      // Instead we use pexpr to prevent conflicts
-        |       ~o~pexpr yP_ORMINUSGT pexpr             { $$ = new AstLogOr{$2, new AstLogNot{$2, $1}, $3}; }
-        |       ~o~pexpr yP_OREQGT pexpr                { $$ = new AstImplication{$2, $1, $3}; }
+        |       ~o~pexpr yP_ORMINUSGT pexpr             { $$ = new AstImplication{$2, $1, $3, true}; }
+        |       ~o~pexpr yP_OREQGT pexpr                { $$ = new AstImplication{$2, $1, $3, false}; }
         //
         //                      // IEEE-2009: property_statement
         //                      // IEEE-2012: yIF and yCASE
@@ -6596,7 +6596,7 @@ sexpr<nodeExprp>:  // ==IEEE: sequence_expr  (The name sexpr is important as reg
         //                      // IEEE: "sequence_expr cycle_delay_range sequence_expr { cycle_delay_range sequence_expr }"
         //                      // Both rules basically mean we can repeat sequences, so make it simpler:
                 cycle_delay_range ~p~sexpr  %prec yP_POUNDPOUND
-                        { $$ = $2; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); DEL($1); }
+                        { $$ = new AstSExpr{$<fl>1, $1, $2}; }
         |       ~p~sexpr cycle_delay_range sexpr %prec prPOUNDPOUND_MULTI
                         { $$ = $1; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); DEL($2, $3); }
         //
@@ -6648,16 +6648,15 @@ sexpr<nodeExprp>:  // ==IEEE: sequence_expr  (The name sexpr is important as reg
         |       BISONPRE_COPY_ONCE(expr,{s/~l~/s/g; s/~p~/s/g; s/~noPar__IGNORE~'.'/yP_PAR__IGNORE /g; })  // {copied}
         ;
 
-cycle_delay_range<nodep>:  // IEEE: ==cycle_delay_range
+cycle_delay_range<delayp>:  // IEEE: ==cycle_delay_range
         //                      // These three terms in 1800-2005 ONLY
                 yP_POUNDPOUND intnumAsConst
-                        { $$ = $2;
-                          BBUNSUP($<fl>1, "Unsupported: ## () cycle delay range expression"); }
+                        { $$ = new AstDelay{$1, $2, true}; }
         |       yP_POUNDPOUND idAny
-                        { $$ = new AstConst{$1, AstConst::BitFalse{}};
+                        { $$ = new AstDelay{$1, new AstConst{$1, AstConst::BitFalse{}}, true};
                           BBUNSUP($<fl>1, "Unsupported: ## id cycle delay range expression"); }
         |       yP_POUNDPOUND '(' constExpr ')'
-                        { $$ = $3;
+                        { $$ = new AstDelay{$1, new AstConst{$1, AstConst::BitFalse{}}, true};
                           BBUNSUP($<fl>1, "Unsupported: ## () cycle delay range expression"); }
         //                      // In 1800-2009 ONLY:
         //                      // IEEE: yP_POUNDPOUND constant_primary
@@ -6665,13 +6664,14 @@ cycle_delay_range<nodep>:  // IEEE: ==cycle_delay_range
         //                      // as ()'s mismatch between primary and the following statement
         //                      // the sv-ac committee has been asked to clarify  (Mantis 1901)
         |       yP_POUNDPOUND anyrange
-                        { $$ = new AstConst{$1, AstConst::BitFalse{}};
-                          BBUNSUP($<fl>1, "Unsupported: ## range cycle delay range expression"); DEL($2); }
+                        { $$ = new AstDelay{$1, new AstConst{$1, AstConst::BitFalse{}}, true};
+                          DEL($2);
+                          BBUNSUP($<fl>1, "Unsupported: ## range cycle delay range expression"); }
         |       yP_POUNDPOUND yP_BRASTAR ']'
-                        { $$ = new AstConst{$1, AstConst::BitFalse{}};
+                        { $$ = new AstDelay{$1, new AstConst{$1, AstConst::BitFalse{}}, true};
                           BBUNSUP($<fl>1, "Unsupported: ## [*] cycle delay range expression"); }
         |       yP_POUNDPOUND yP_BRAPLUSKET
-                        { $$ = new AstConst{$1, AstConst::BitFalse{}};
+                        { $$ = new AstDelay{$1, new AstConst{$1, AstConst::BitFalse{}}, true};
                           BBUNSUP($<fl>1, "Unsupported: ## [+] cycle delay range expression"); }
         ;
 
diff --git a/test_regress/t/t_debug_emitv.out b/test_regress/t/t_debug_emitv.out
index 6328c36ec..aedb5a5ea 100644
--- a/test_regress/t/t_debug_emitv.out
+++ b/test_regress/t/t_debug_emitv.out
@@ -74,7 +74,7 @@ module Vt_debug_emitv_t;
             if (the_ifaces[2].ifsig) begin
                 $write("");
             end
-            #64'h1;
+            #1;
             $write("After #1 delay");
         end
     end
@@ -359,6 +359,311 @@ module Vt_debug_emitv_t;
             release sum;
         end
     end
+    property p;
+    @(posedge clk) ##1 sum[0]
+    endproperty
+    property p1;
+    @( clk) sum[0]
+    endproperty
+    property p2;
+    @(posedge clk) disable iff (cyc == 'sh1) ##1 sum[0]
+    endproperty
+    assert property (@( clk) (! ##1 in)
+    ) begin
+    end
+    else begin
+    end
+    initial begin
+        begin
+            begin : assert_simple_immediate_else
+                assert ('sh0) begin
+                end
+                else begin
+                    $display("fail");
+                end
+            end
+            begin : assert_simple_immediate_stmt
+                assert ('sh0) begin
+                    $display("pass");
+                end
+                else begin
+                end
+            end
+            begin : assert_simple_immediate_stmt_else
+                assert ('sh0) begin
+                    $display("pass");
+                end
+                else begin
+                    $display("fail");
+                end
+            end
+            begin : assume_simple_immediate
+                assume ('sh0) begin
+                end
+                else begin
+                end
+            end
+            begin : assume_simple_immediate_else
+                assume ('sh0) begin
+                end
+                else begin
+                    $display("fail");
+                end
+            end
+            begin : assume_simple_immediate_stmt
+                assume ('sh0) begin
+                    $display("pass");
+                end
+                else begin
+                end
+            end
+            begin : assume_simple_immediate_stmt_else
+                assume ('sh0) begin
+                    $display("pass");
+                end
+                else begin
+                    $display("fail");
+                end
+            end
+        end
+    end
+    always  begin
+        begin : assert_observed_deferred_immediate
+            assert #0 ('sh0) begin
+            end
+            else begin
+            end
+        end
+    end
+    always  begin
+        begin : assert_observed_deferred_immediate_else
+            assert #0 ('sh0) begin
+            end
+            else begin
+                $display("fail");
+            end
+        end
+    end
+    always  begin
+        begin : assert_observed_deferred_immediate_stmt
+            assert #0 ('sh0) begin
+                $display("pass");
+            end
+            else begin
+            end
+        end
+    end
+    always  begin
+        begin : assert_observed_deferred_immediate_stmt_else
+            assert #0 ('sh0) begin
+                $display("pass");
+            end
+            else begin
+                $display("fail");
+            end
+        end
+    end
+    always  begin
+        begin : assume_observed_deferred_immediate
+            assume #0 ('sh0) begin
+            end
+            else begin
+            end
+        end
+    end
+    always  begin
+        begin : assume_observed_deferred_immediate_else
+            assume #0 ('sh0) begin
+            end
+            else begin
+                $display("fail");
+            end
+        end
+    end
+    always  begin
+        begin : assume_observed_deferred_immediate_stmt
+            assume #0 ('sh0) begin
+                $display("pass");
+            end
+            else begin
+            end
+        end
+    end
+    always  begin
+        begin : assume_observed_deferred_immediate_stmt_else
+            assume #0 ('sh0) begin
+                $display("pass");
+            end
+            else begin
+                $display("fail");
+            end
+        end
+    end
+    always  begin
+        begin : assert_final_deferred_immediate
+            assert final ('sh0) begin
+            end
+            else begin
+            end
+        end
+    end
+    always  begin
+        begin : assert_final_deferred_immediate_else
+            assert final ('sh0) begin
+            end
+            else begin
+                $display("fail");
+            end
+        end
+    end
+    always  begin
+        begin : assert_final_deferred_immediate_stmt
+            assert final ('sh0) begin
+                $display("pass");
+            end
+            else begin
+            end
+        end
+    end
+    always  begin
+        begin : assert_final_deferred_immediate_stmt_else
+            assert final ('sh0) begin
+                $display("pass");
+            end
+            else begin
+                $display("fail");
+            end
+        end
+    end
+    always  begin
+        begin : assume_final_deferred_immediate
+            assume final ('sh0) begin
+            end
+            else begin
+            end
+        end
+    end
+    always  begin
+        begin : assume_final_deferred_immediate_else
+            assume final ('sh0) begin
+            end
+            else begin
+                $display("fail");
+            end
+        end
+    end
+    always  begin
+        begin : assume_final_deferred_immediate_stmt
+            assume final ('sh0) begin
+                $display("pass");
+            end
+            else begin
+            end
+        end
+    end
+    always  begin
+        begin : assume_final_deferred_immediate_stmt_else
+            assume final ('sh0) begin
+                $display("pass");
+            end
+            else begin
+                $display("fail");
+            end
+        end
+    end
+    property prop;
+    @(posedge clk) 'sh0
+    endproperty
+    begin : assert_concurrent
+        assert property ( prop
+        ) begin
+        end
+        else begin
+        end
+    end
+    begin : assert_concurrent_else
+        assert property ( prop
+        ) begin
+        end
+        else begin
+            $display("fail");
+        end
+    end
+    begin : assert_concurrent_stmt
+        assert property ( prop
+        ) begin
+            $display("pass");
+        end
+        else begin
+        end
+    end
+    begin : assert_concurrent_stmt_else
+        assert property ( prop
+        ) begin
+            $display("pass");
+        end
+        else begin
+            $display("fail");
+        end
+    end
+    begin : assume_concurrent
+        assume property ( prop
+        ) begin
+        end
+        else begin
+        end
+    end
+    begin : assume_concurrent_else
+        assume property ( prop
+        ) begin
+        end
+        else begin
+            $display("fail");
+        end
+    end
+    begin : assume_concurrent_stmt
+        assume property ( prop
+        ) begin
+            $display("pass");
+        end
+        else begin
+        end
+    end
+    begin : assume_concurrent_stmt_else
+        assume property ( prop
+        ) begin
+            $display("pass");
+        end
+        else begin
+            $display("fail");
+        end
+    end
+    begin : cover_concurrent
+        cover property ( prop
+        ) begin
+        end
+    end
+    begin : cover_concurrent_stmt
+        cover property ( prop
+        ) begin
+            $display("pass");
+        end
+    end
+    int signed a;
+    int signed ao;
+    initial begin
+        begin : assert_intrinsic
+            assert ((| $_EXPRSTMT(
+                        ao = (a);
+                        , );
+                )) begin
+            end
+            else begin
+            end
+        end
+    end
+    restrict (@(posedge clk) ##1 a[0]
+    );
 endmodule
 package Vt_debug_emitv___024unit;
     class Vt_debug_emitv_Cls;
diff --git a/test_regress/t/t_debug_emitv.v b/test_regress/t/t_debug_emitv.v
index 36761f2dc..0b3a79f68 100644
--- a/test_regress/t/t_debug_emitv.v
+++ b/test_regress/t/t_debug_emitv.v
@@ -269,6 +269,77 @@ module t (/*AUTOARG*/
       repeat (2) if (sum != 10) $stop;
       release sum;
    end
+
+   property p;
+      @(posedge clk) ##1 sum[0]
+   endproperty
+   property p1;
+      @(clk) sum[0]
+   endproperty
+   property p2;
+      @(posedge clk) disable iff (cyc == 1) ##1 sum[0]
+   endproperty
+
+   assert property (@(clk) not ##1 in);
+
+   initial begin
+      assert_simple_immediate_else: assert(0) else $display("fail");
+      assert_simple_immediate_stmt: assert(0) $display("pass");
+      assert_simple_immediate_stmt_else: assert(0) $display("pass"); else $display("fail");
+
+      assume_simple_immediate: assume(0);
+      assume_simple_immediate_else: assume(0) else $display("fail");
+      assume_simple_immediate_stmt: assume(0) $display("pass");
+      assume_simple_immediate_stmt_else: assume(0) $display("pass"); else $display("fail");
+   end
+
+   assert_observed_deferred_immediate: assert #0 (0);
+   assert_observed_deferred_immediate_else: assert #0 (0) else $display("fail");
+   assert_observed_deferred_immediate_stmt: assert #0 (0) $display("pass");
+   assert_observed_deferred_immediate_stmt_else: assert #0 (0) $display("pass"); else $display("fail");
+
+   assume_observed_deferred_immediate: assume #0 (0);
+   assume_observed_deferred_immediate_else: assume #0 (0) else $display("fail");
+   assume_observed_deferred_immediate_stmt: assume #0 (0) $display("pass");
+   assume_observed_deferred_immediate_stmt_else: assume #0 (0) $display("pass"); else $display("fail");
+
+   assert_final_deferred_immediate: assert final (0);
+   assert_final_deferred_immediate_else: assert final (0) else $display("fail");
+   assert_final_deferred_immediate_stmt: assert final (0) $display("pass");
+   assert_final_deferred_immediate_stmt_else: assert final (0) $display("pass"); else $display("fail");
+
+   assume_final_deferred_immediate: assume final (0);
+   assume_final_deferred_immediate_else: assume final (0) else $display("fail");
+   assume_final_deferred_immediate_stmt: assume final (0) $display("pass");
+   assume_final_deferred_immediate_stmt_else: assume final (0) $display("pass"); else $display("fail");
+
+   property prop();
+      @(posedge clk) 0
+   endproperty
+
+   assert_concurrent: assert property (prop);
+   assert_concurrent_else: assert property(prop) else $display("fail");
+   assert_concurrent_stmt: assert property(prop) $display("pass");
+   assert_concurrent_stmt_else: assert property(prop) $display("pass"); else $display("fail");
+
+   assume_concurrent: assume property(prop);
+   assume_concurrent_else: assume property(prop) else $display("fail");
+   assume_concurrent_stmt: assume property(prop) $display("pass");
+   assume_concurrent_stmt_else: assume property(prop) $display("pass"); else $display("fail");
+
+   cover_concurrent: cover property(prop);
+   cover_concurrent_stmt: cover property(prop) $display("pass");
+
+
+   int a;
+   int ao;
+
+   // verilator lint_off CASTCONST
+   initial begin : assert_intrinsic
+      $cast(ao, a);
+   end
+
+   restrict property (@(posedge clk) ##1 a[0]);
 endmodule
 
 module sub(input logic clk);
diff --git a/test_regress/t/t_dist_copyright.py b/test_regress/t/t_dist_copyright.py
index 283f77a42..2550a5d23 100755
--- a/test_regress/t/t_dist_copyright.py
+++ b/test_regress/t/t_dist_copyright.py
@@ -44,6 +44,7 @@ EXEMPT_FILES_LIST = """
     test_regress/t/t_fuzz_eof_bad.v
     test_regress/t/t_incr_void.v
     test_regress/t/t_property_unsup.v
+    test_regress/t/t_sequence_first_match_unsup.v
     test_regress/t/tsub/t_flag_f_tsub.v
     test_regress/t/tsub/t_flag_f_tsub_inc.v
     test_regress/t/uvm/dpi
diff --git a/test_regress/t/t_expect.out b/test_regress/t/t_expect.out
index 5df2a5f91..5f7f2d122 100644
--- a/test_regress/t/t_expect.out
+++ b/test_regress/t/t_expect.out
@@ -1,28 +1,19 @@
-%Error-UNSUPPORTED: t/t_expect.v:19:32: Unsupported: ## () cycle delay range expression
+%Error-UNSUPPORTED: t/t_expect.v:19:32: Unsupported: ## (in sequence expression)
    19 |       expect (@(posedge clk) a ##1 b) a = 110;
       |                                ^~
                     ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
-%Error-UNSUPPORTED: t/t_expect.v:19:34: Unsupported: ## (in sequence expression)
-   19 |       expect (@(posedge clk) a ##1 b) a = 110;
-      |                                  ^
 %Error-UNSUPPORTED: t/t_expect.v:19:7: Unsupported: expect
    19 |       expect (@(posedge clk) a ##1 b) a = 110;
       |       ^~~~~~
-%Error-UNSUPPORTED: t/t_expect.v:21:32: Unsupported: ## () cycle delay range expression
+%Error-UNSUPPORTED: t/t_expect.v:21:32: Unsupported: ## (in sequence expression)
    21 |       expect (@(posedge clk) a ##1 b) else a = 299;
       |                                ^~
-%Error-UNSUPPORTED: t/t_expect.v:21:34: Unsupported: ## (in sequence expression)
-   21 |       expect (@(posedge clk) a ##1 b) else a = 299;
-      |                                  ^
 %Error-UNSUPPORTED: t/t_expect.v:21:7: Unsupported: expect
    21 |       expect (@(posedge clk) a ##1 b) else a = 299;
       |       ^~~~~~
-%Error-UNSUPPORTED: t/t_expect.v:23:32: Unsupported: ## () cycle delay range expression
+%Error-UNSUPPORTED: t/t_expect.v:23:32: Unsupported: ## (in sequence expression)
    23 |       expect (@(posedge clk) a ##1 b) a = 300; else a = 399;
       |                                ^~
-%Error-UNSUPPORTED: t/t_expect.v:23:34: Unsupported: ## (in sequence expression)
-   23 |       expect (@(posedge clk) a ##1 b) a = 300; else a = 399;
-      |                                  ^
 %Error-UNSUPPORTED: t/t_expect.v:23:7: Unsupported: expect
    23 |       expect (@(posedge clk) a ##1 b) a = 300; else a = 399;
       |       ^~~~~~
diff --git a/test_regress/t/t_property_sexpr.out b/test_regress/t/t_property_sexpr.out
new file mode 100644
index 000000000..7f65a6dfc
--- /dev/null
+++ b/test_regress/t/t_property_sexpr.out
@@ -0,0 +1,140 @@
+[4] single delay with const stmt, fileline:115
+[5] concurrent assert else, fileline:167
+[6] single delay with const stmt, fileline:115
+[7] concurrent assert stmt, fileline:166
+[8] single delay with const stmt, fileline:115
+[9] concurrent assert else, fileline:167
+[11] concurrent assert else, fileline:167
+[12] single delay with var stmt, fileline:118
+[13] concurrent assert else, fileline:167
+[14] single delay with var else, fileline:119
+[15] concurrent assert stmt, fileline:166
+[16] single delay with var stmt, fileline:118
+[17] concurrent assert else, fileline:167
+[18] single delay with var else, fileline:119
+[19] concurrent assert else, fileline:167
+[20] single delay with var stmt, fileline:118
+[21] concurrent assert else, fileline:167
+[23] concurrent assert stmt, fileline:166
+[25] concurrent assert else, fileline:167
+[26] single multi-cycle delay with var else, fileline:123
+[27] concurrent assert else, fileline:167
+[28] single multi-cycle delay with var stmt, fileline:122
+[29] concurrent assert else, fileline:167
+[30] single multi-cycle delay with var else, fileline:123
+[31] concurrent assert stmt, fileline:166
+[33] concurrent assert else, fileline:167
+[34] single delay with var brackets 1 else, fileline:127
+[35] concurrent assert else, fileline:167
+[36] single delay with var brackets 1 stmt, fileline:126
+[37] concurrent assert else, fileline:167
+[38] single delay with var brackets 1 else, fileline:127
+[39] concurrent assert stmt, fileline:166
+[40] single delay with var brackets 1 stmt, fileline:126
+[41] concurrent assert else, fileline:167
+[43] concurrent assert else, fileline:167
+[44] single delay with var brackets 2 stmt, fileline:130
+[45] concurrent assert else, fileline:167
+[46] single delay with var brackets 2 else, fileline:131
+[47] concurrent assert stmt, fileline:166
+[48] single delay with var brackets 2 stmt, fileline:130
+[49] concurrent assert else, fileline:167
+[50] single delay with var brackets 2 else, fileline:131
+[51] concurrent assert else, fileline:167
+[53] concurrent assert else, fileline:167
+[54] single delay with negated var else, fileline:135
+[55] concurrent assert stmt, fileline:166
+[56] single delay with negated var stmt, fileline:134
+[57] concurrent assert else, fileline:167
+[58] single delay with negated var else, fileline:135
+[59] concurrent assert else, fileline:167
+[60] single delay with negated var else, fileline:135
+[61] concurrent assert else, fileline:167
+[63] concurrent assert stmt, fileline:166
+[64] single delay with negated var else, fileline:139
+[65] concurrent assert else, fileline:167
+[66] single delay with negated var stmt, fileline:138
+[67] concurrent assert else, fileline:167
+[68] single delay with negated var else, fileline:139
+[69] concurrent assert else, fileline:167
+[70] single delay with negated var stmt, fileline:138
+[71] concurrent assert stmt, fileline:166
+[73] concurrent assert else, fileline:167
+[74] single delay with negated var brackets stmt, fileline:142
+[75] concurrent assert else, fileline:167
+[76] single delay with negated var brackets else, fileline:144
+[77] concurrent assert else, fileline:167
+[78] single delay with negated var brackets stmt, fileline:142
+[79] concurrent assert stmt, fileline:166
+[80] single delay with negated var brackets else, fileline:144
+[81] concurrent assert else, fileline:167
+[83] concurrent assert else, fileline:167
+[84] single delay with negated var brackets else, fileline:148
+[85] concurrent assert else, fileline:167
+[87] concurrent assert stmt, fileline:166
+[88] single delay with negated var brackets else, fileline:148
+[89] concurrent assert else, fileline:167
+[91] concurrent assert else, fileline:167
+[93] concurrent assert else, fileline:167
+[94] single delay with nested not else, fileline:152
+[95] concurrent assert stmt, fileline:166
+[96] single delay with nested not stmt, fileline:151
+[97] concurrent assert else, fileline:167
+[98] single delay with nested not else, fileline:152
+[99] concurrent assert else, fileline:167
+[100] single delay with nested not stmt, fileline:151
+[101] concurrent assert else, fileline:167
+[103] concurrent assert stmt, fileline:166
+[105] concurrent assert else, fileline:167
+[107] concurrent assert else, fileline:167
+[109] concurrent assert else, fileline:167
+[111] concurrent assert stmt, fileline:166
+[113] concurrent assert else, fileline:167
+[114] property, fileline:162
+[115] concurrent assert else, fileline:167
+[116] property, fileline:163
+[117] concurrent assert else, fileline:167
+[118] property, fileline:162
+[119] concurrent assert stmt, fileline:166
+[120] property, fileline:163
+[121] concurrent assert else, fileline:167
+[123] concurrent assert else, fileline:167
+[125] concurrent assert else, fileline:167
+[127] concurrent assert stmt, fileline:166
+[129] concurrent assert else, fileline:167
+[131] concurrent assert else, fileline:167
+[133] concurrent assert else, fileline:167
+[135] concurrent assert stmt, fileline:166
+[137] concurrent assert else, fileline:167
+[139] concurrent assert else, fileline:167
+[141] concurrent assert else, fileline:167
+[143] concurrent assert stmt, fileline:166
+[145] concurrent assert else, fileline:167
+[147] concurrent assert else, fileline:167
+[149] concurrent assert else, fileline:167
+[151] concurrent assert stmt, fileline:166
+[153] concurrent assert else, fileline:167
+[155] concurrent assert else, fileline:167
+[157] concurrent assert else, fileline:167
+[159] concurrent assert stmt, fileline:166
+[161] concurrent assert else, fileline:167
+[163] concurrent assert else, fileline:167
+[165] concurrent assert else, fileline:167
+[167] concurrent assert stmt, fileline:166
+[169] concurrent assert else, fileline:167
+[171] concurrent assert else, fileline:167
+[173] concurrent assert else, fileline:167
+[175] concurrent assert stmt, fileline:166
+[177] concurrent assert else, fileline:167
+[179] concurrent assert else, fileline:167
+[181] concurrent assert else, fileline:167
+[183] concurrent assert stmt, fileline:166
+[185] concurrent assert else, fileline:167
+[187] concurrent assert else, fileline:167
+[189] concurrent assert else, fileline:167
+[191] concurrent assert stmt, fileline:166
+[193] concurrent assert else, fileline:167
+[195] concurrent assert else, fileline:167
+[197] concurrent assert else, fileline:167
+[199] concurrent assert stmt, fileline:166
+*-* All Finished *-*
diff --git a/test_regress/t/t_property_sexpr.py b/test_regress/t/t_property_sexpr.py
new file mode 100755
index 000000000..786072909
--- /dev/null
+++ b/test_regress/t/t_property_sexpr.py
@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# Copyright 2025 by Wilson Snyder. This program is free software; you
+# can redistribute it and/or modify it under the terms of either the GNU
+# Lesser General Public License Version 3 or the Perl Artistic License
+# Version 2.0.
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('simulator')
+
+test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing'])
+
+test.execute(expect_filename=test.golden_filename)
+
+test.passes()
diff --git a/test_regress/t/t_property_sexpr.v b/test_regress/t/t_property_sexpr.v
new file mode 100644
index 000000000..7dd5a3801
--- /dev/null
+++ b/test_regress/t/t_property_sexpr.v
@@ -0,0 +1,168 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed into the Public Domain, for any use,
+// without warranty, 2025 by Antmicro.
+// SPDX-License-Identifier: CC0-1.0
+
+module t (  /*AUTOARG*/
+    // Inputs
+    clk
+);
+
+  input clk;
+
+  bit [3:0] val = 0;
+  event e1;
+  event e2;
+  event e3;
+  event e4;
+  event e5;
+  event e6;
+  event e7;
+  event e8;
+  event e9;
+  event e10;
+  event e11;
+  event e12;
+  integer cyc = 1;
+
+  always @(negedge clk) begin
+    val <= 4'(cyc % 4);
+
+    if (cyc >= 0 && cyc <= 4) begin
+      ->e1;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e1", $time);
+`endif
+    end
+    if (cyc >= 5 && cyc <= 10) begin
+      ->e2;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e2", $time);
+`endif
+    end
+    if (cyc >= 11 && cyc <= 15) begin
+      ->e3;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e3", $time);
+`endif
+    end
+    if (cyc >= 16 && cyc <= 20) begin
+      ->e4;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e4", $time);
+`endif
+    end
+    if (cyc >= 21 && cyc <= 25) begin
+      ->e5;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e5", $time);
+`endif
+    end
+    if (cyc >= 26 && cyc <= 30) begin
+      ->e6;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e6", $time);
+`endif
+    end
+    if (cyc >= 31 && cyc <= 35) begin
+      ->e7;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e7", $time);
+`endif
+    end
+    if (cyc >= 36 && cyc <= 40) begin
+      ->e8;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e8", $time);
+`endif
+    end
+    if (cyc >= 41 && cyc <= 45) begin
+      ->e9;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e9", $time);
+`endif
+    end
+    if (cyc >= 46 && cyc <= 50) begin
+      ->e10;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e10", $time);
+`endif
+    end
+    if (cyc >= 51 && cyc <= 55) begin
+      ->e11;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e11", $time);
+`endif
+    end
+    if (cyc >= 56 && cyc <= 60) begin
+      ->e12;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e12", $time);
+`endif
+    end
+`ifdef TEST_VERBOSE
+    $display("cyc=%0d val=%0d", cyc, val);
+`endif
+    cyc <= cyc + 1;
+    if (cyc == 100) begin
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+  assert property (@(e1) ##1 1)
+    $display("[%0t] single delay with const stmt, fileline:%0d", $time, `__LINE__);
+
+  assert property (@(e2) ##1 val[0])
+    $display("[%0t] single delay with var stmt, fileline:%0d", $time, `__LINE__);
+  else $display("[%0t] single delay with var else, fileline:%0d", $time, `__LINE__);
+
+  assert property (@(e3) ##2 val[0])
+    $display("[%0t] single multi-cycle delay with var stmt, fileline:%0d", $time, `__LINE__);
+  else $display("[%0t] single multi-cycle delay with var else, fileline:%0d", $time, `__LINE__);
+
+  assert property (@(e4) ##1 (val[0]))
+    $display("[%0t] single delay with var brackets 1 stmt, fileline:%0d", $time, `__LINE__);
+  else $display("[%0t] single delay with var brackets 1 else, fileline:%0d", $time, `__LINE__);
+
+  assert property (@(e5) (##1 (val[0])))
+    $display("[%0t] single delay with var brackets 2 stmt, fileline:%0d", $time, `__LINE__);
+  else $display("[%0t] single delay with var brackets 2 else, fileline:%0d", $time, `__LINE__);
+
+  assert property (@(e6) (##1 val[0] && val[1]))
+    $display("[%0t] single delay with negated var stmt, fileline:%0d", $time, `__LINE__);
+  else $display("[%0t] single delay with negated var else, fileline:%0d", $time, `__LINE__);
+
+  assert property (@(e7) not ##1 val[0])
+    $display("[%0t] single delay with negated var stmt, fileline:%0d", $time, `__LINE__);
+  else $display("[%0t] single delay with negated var else, fileline:%0d", $time, `__LINE__);
+
+  assume property (@(e8) not (##1 val[0]))
+    $display("[%0t] single delay with negated var brackets stmt, fileline:%0d", $time, `__LINE__);
+  else
+    $display("[%0t] single delay with negated var brackets else, fileline:%0d", $time, `__LINE__);
+
+  assume property (@(e9) not (##1 val[0]))
+  else
+    $display("[%0t] single delay with negated var brackets else, fileline:%0d", $time, `__LINE__);
+
+  assert property (@(e10) not (not ##1 val[0]))
+    $display("[%0t] single delay with nested not stmt, fileline:%0d", $time, `__LINE__);
+  else $display("[%0t] single delay with nested not else, fileline:%0d", $time, `__LINE__);
+
+  restrict property (@(e11) ##1 val[0]);
+
+  restrict property (@(e11) not ##1 val[0]);
+
+  property prop;
+    @(e12) not ##1 val[0]
+  endproperty
+
+  assert property (prop) $display("[%0t] property, fileline:%0d", $time, `__LINE__);
+  else $display("[%0t] property, fileline:%0d", $time, `__LINE__);
+
+  assert property (@(posedge clk) not (not ##2 val[0] && val[1]))
+    $display("[%0t] concurrent assert stmt, fileline:%0d", $time, `__LINE__);
+  else $display("[%0t] concurrent assert else, fileline:%0d", $time, `__LINE__);
+endmodule
diff --git a/test_regress/t/t_property_sexpr_bad.out b/test_regress/t/t_property_sexpr_bad.out
new file mode 100644
index 000000000..7b7051080
--- /dev/null
+++ b/test_regress/t/t_property_sexpr_bad.out
@@ -0,0 +1,6 @@
+%Error: t/t_property_sexpr_bad.v:20:39: Syntax error: unexpected 'not' in sequence expression
+                                      : ... note: In instance 't'
+   20 |   assert property (@(posedge clk) ##1 not val) $display("[%0t] single delay with negated var stmt, fileline:%d", $time, 20);
+      |                                       ^~~
+        ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
+%Error: Exiting due to
diff --git a/test_regress/t/t_property_sexpr_bad.py b/test_regress/t/t_property_sexpr_bad.py
new file mode 100755
index 000000000..5562c90e9
--- /dev/null
+++ b/test_regress/t/t_property_sexpr_bad.py
@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# Copyright 2025 by Wilson Snyder. This program is free software; you
+# can redistribute it and/or modify it under the terms of either the GNU
+# Lesser General Public License Version 3 or the Perl Artistic License
+# Version 2.0.
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt')
+
+test.lint(fails=True,
+          verilator_flags2=['--assert', '--timing'],
+          expect_filename=test.golden_filename)
+
+test.passes()
diff --git a/test_regress/t/t_property_sexpr_bad.v b/test_regress/t/t_property_sexpr_bad.v
new file mode 100644
index 000000000..86936c100
--- /dev/null
+++ b/test_regress/t/t_property_sexpr_bad.v
@@ -0,0 +1,21 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed into the Public Domain, for any use,
+// without warranty, 2025 by Antmicro.
+// SPDX-License-Identifier: CC0-1.0
+
+module t (  /*AUTOARG*/
+    // Inputs
+    clk
+);
+
+  input clk;
+  bit val;
+
+  always @(negedge clk) begin
+    $write("*-* All Finished *-*\n");
+    $finish;
+  end
+
+  assert property (@(posedge clk) ##1 not val) $display("[%0t] single delay with negated var stmt, fileline:%d", $time, `__LINE__);
+endmodule
diff --git a/test_regress/t/t_property_sexpr_cov.out b/test_regress/t/t_property_sexpr_cov.out
new file mode 100644
index 000000000..2397081f7
--- /dev/null
+++ b/test_regress/t/t_property_sexpr_cov.out
@@ -0,0 +1,31 @@
+[4] cover property, fileline:45
+[7] concurrent cover, fileline:51
+[8] cover property, fileline:45
+[12] not cover property, fileline:48
+[15] concurrent cover, fileline:51
+[18] not cover property, fileline:48
+[20] not cover property, fileline:48
+[23] concurrent cover, fileline:51
+[31] concurrent cover, fileline:51
+[39] concurrent cover, fileline:51
+[47] concurrent cover, fileline:51
+[55] concurrent cover, fileline:51
+[63] concurrent cover, fileline:51
+[71] concurrent cover, fileline:51
+[79] concurrent cover, fileline:51
+[87] concurrent cover, fileline:51
+[95] concurrent cover, fileline:51
+[103] concurrent cover, fileline:51
+[111] concurrent cover, fileline:51
+[119] concurrent cover, fileline:51
+[127] concurrent cover, fileline:51
+[135] concurrent cover, fileline:51
+[143] concurrent cover, fileline:51
+[151] concurrent cover, fileline:51
+[159] concurrent cover, fileline:51
+[167] concurrent cover, fileline:51
+[175] concurrent cover, fileline:51
+[183] concurrent cover, fileline:51
+[191] concurrent cover, fileline:51
+[199] concurrent cover, fileline:51
+*-* All Finished *-*
diff --git a/test_regress/t/t_property_sexpr_cov.py b/test_regress/t/t_property_sexpr_cov.py
new file mode 100755
index 000000000..d48d60eb6
--- /dev/null
+++ b/test_regress/t/t_property_sexpr_cov.py
@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# Copyright 2025 by Wilson Snyder. This program is free software; you
+# can redistribute it and/or modify it under the terms of either the GNU
+# Lesser General Public License Version 3 or the Perl Artistic License
+# Version 2.0.
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('simulator')
+
+test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing', '--coverage-user'])
+
+test.execute(expect_filename=test.golden_filename)
+
+test.passes()
diff --git a/test_regress/t/t_property_sexpr_cov.v b/test_regress/t/t_property_sexpr_cov.v
new file mode 100644
index 000000000..57506da30
--- /dev/null
+++ b/test_regress/t/t_property_sexpr_cov.v
@@ -0,0 +1,52 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed into the Public Domain, for any use,
+// without warranty, 2025 by Antmicro.
+// SPDX-License-Identifier: CC0-1.0
+
+module t (  /*AUTOARG*/
+    // Inputs
+    clk
+);
+
+  input clk;
+
+  bit [3:0] val = 0;
+  event e1;
+  event e2;
+  integer cyc = 1;
+
+  always @(negedge clk) begin
+    val <= 4'(cyc % 4);
+
+    if (cyc >= 0 && cyc <= 4) begin
+      ->e1;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e1", $time);
+`endif
+    end
+    if (cyc >= 5 && cyc <= 10) begin
+      ->e2;
+`ifdef TEST_VERBOSE
+      $display("[%0t] triggered e2", $time);
+`endif
+    end
+`ifdef TEST_VERBOSE
+    $display("cyc=%0d val=%0d", cyc, val);
+`endif
+    cyc <= cyc + 1;
+    if (cyc == 100) begin
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+  cover property (@(e1) ##1 val[0])
+    $display("[%0t] cover property, fileline:%0d", $time, `__LINE__);
+
+  cover property (@(e2) not ##1 val[1])
+    $display("[%0t] not cover property, fileline:%0d", $time, `__LINE__);
+
+  cover property (@(posedge clk) ##3 val[0] && val[1])
+    $display("[%0t] concurrent cover, fileline:%0d", $time, `__LINE__);
+endmodule
diff --git a/test_regress/t/t_property_sexpr_parse_unsup.out b/test_regress/t/t_property_sexpr_parse_unsup.out
new file mode 100644
index 000000000..5b77f4421
--- /dev/null
+++ b/test_regress/t/t_property_sexpr_parse_unsup.out
@@ -0,0 +1,35 @@
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:29:39: Unsupported: ## (in sequence expression)
+   29 |   assert property (@(posedge clk) val ##1 val) $display("[%0t] var with single delay stmt, fileline:%d", $time, 29);
+      |                                       ^~
+                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:30:43: Unsupported: ## (in sequence expression)
+   30 |   assert property (@(posedge clk) ##1 val ##2 val) $display("[%0t] sequence stmt, fileline:%d", $time, 30);
+      |                                           ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:71:14: Unsupported sequence match items
+   71 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
+      |              ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:71:29: Unsupported: ## range cycle delay range expression
+   71 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
+      |                             ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:70:13: Unsupported: property variable declaration
+   70 |     integer l_b;
+      |             ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:16: Unsupported sequence match items
+   88 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+      |                ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:51: Unsupported: [-> boolean abbrev expression
+   88 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+      |                                                   ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:54: Unsupported: boolean abbrev (in sequence expression)
+   88 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+      |                                                      ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:35: Unsupported: ## (in sequence expression)
+   88 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+      |                                   ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:86:14: Unsupported: property variable declaration
+   86 |     realtime l_t;
+      |              ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:31: Unsupported: ## (in sequence expression)
+   92 |   assert property (@clk not a ##1 b);
+      |                               ^~
+%Error: Exiting due to
diff --git a/test_regress/t/t_property_sexpr_parse_unsup.py b/test_regress/t/t_property_sexpr_parse_unsup.py
new file mode 100755
index 000000000..6f175f1ac
--- /dev/null
+++ b/test_regress/t/t_property_sexpr_parse_unsup.py
@@ -0,0 +1,20 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# Copyright 2025 by Wilson Snyder. This program is free software; you
+# can redistribute it and/or modify it under the terms of either the GNU
+# Lesser General Public License Version 3 or the Perl Artistic License
+# Version 2.0.
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('vlt')
+
+test.top_filename = "t/t_property_sexpr_unsup.v"
+
+test.lint(expect_filename=test.golden_filename,
+          verilator_flags2=['-DPARSING_TIME', '--assert', '--timing', '--error-limit 1000'],
+          fails=True)
+
+test.passes()
diff --git a/test_regress/t/t_property_sexpr_unsup.out b/test_regress/t/t_property_sexpr_unsup.out
index aa80d23e8..367002cf4 100644
--- a/test_regress/t/t_property_sexpr_unsup.out
+++ b/test_regress/t/t_property_sexpr_unsup.out
@@ -1,122 +1,35 @@
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:46:35: Unsupported: ## () cycle delay range expression
-   46 |   assert property (@(posedge clk) ##2 val)
-      |                                   ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:32:41: Unsupported: Implication with sequence expression
+   32 |   assert property (@(posedge clk) ##1 1 |-> 1) $display("[%0t] single delay with const implication stmt, fileline:%d", $time, 32);
+      |                                         ^~~
                     ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:46:39: Unsupported: ## (in sequence expression)
-   46 |   assert property (@(posedge clk) ##2 val)
-      |                                       ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:35: Unsupported: ## () cycle delay range expression
-   49 |   assert property (@(posedge clk) ##1 1 |=> 0)
-      |                                   ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:39: Unsupported: ## (in sequence expression)
-   49 |   assert property (@(posedge clk) ##1 1 |=> 0)
-      |                                       ^
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:35: Unsupported: ## () cycle delay range expression
-   52 |   assert property (@(posedge clk) ##1 1 |=> not (val))
-      |                                   ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:39: Unsupported: ## (in sequence expression)
-   52 |   assert property (@(posedge clk) ##1 1 |=> not (val))
-      |                                       ^
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:35: Unsupported: ## () cycle delay range expression
-   55 |   assert property (@(posedge clk) ##1 val)
-      |                                   ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:39: Unsupported: ## (in sequence expression)
-   55 |   assert property (@(posedge clk) ##1 val)
-      |                                       ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:58:35: Unsupported: ## () cycle delay range expression
-   58 |   assert property (@(posedge clk) ##1 (val))
-      |                                   ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:58:40: Unsupported: ## (in sequence expression)
-   58 |   assert property (@(posedge clk) ##1 (val))
-      |                                        ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:61:36: Unsupported: ## () cycle delay range expression
-   61 |   assert property (@(posedge clk) (##1 (val)))
-      |                                    ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:61:41: Unsupported: ## (in sequence expression)
-   61 |   assert property (@(posedge clk) (##1 (val)))
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:34:41: Unsupported: Implication with sequence expression
+   34 |   assert property (@(posedge clk) ##1 1 |-> not (val)) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, 34);
       |                                         ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:64:36: Unsupported: ## () cycle delay range expression
-   64 |   assert property (@(posedge clk) (##1 (val)))
-      |                                    ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:64:41: Unsupported: ## (in sequence expression)
-   64 |   assert property (@(posedge clk) (##1 (val)))
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:36:37: Unsupported: Implication with sequence expression
+   36 |   assert property (@(posedge clk) 1 |-> ##1 val) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, 36);
+      |                                     ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:38:45: Unsupported: Implication with sequence expression
+   38 |   assert property (@(posedge clk) (##1 val) |-> (not val)) $display("[%0t] single delay with negated implication stmt, fileline:%d", $time, 38);
+      |                                             ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:40:45: Unsupported: Implication with sequence expression
+   40 |   assert property (@(posedge clk) ##1 (val) |-> not (val)) $display("[%0t] single delay with negated implication brackets stmt, fileline:%d", $time, 40);
+      |                                             ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:44:41: Unsupported: Implication with sequence expression
+   44 |   assert property (@(posedge clk) ##1 1 |-> 0) $display("[%0t] disable iff with cond implication stmt, fileline:%d", $time, 44);
       |                                         ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:67:40: Unsupported: ## () cycle delay range expression
-   67 |   assert property (@(posedge clk) not (##1 val))
-      |                                        ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:67:44: Unsupported: ## (in sequence expression)
-   67 |   assert property (@(posedge clk) not (##1 val))
-      |                                            ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:70:35: Unsupported: ## () cycle delay range expression
-   70 |   assert property (@(posedge clk) ##1 1 |=> 1)
-      |                                   ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:70:39: Unsupported: ## (in sequence expression)
-   70 |   assert property (@(posedge clk) ##1 1 |=> 1)
-      |                                       ^
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:73:35: Unsupported: ## () cycle delay range expression
-   73 |   assert property (@(posedge clk) ##1 val |=> not val)
-      |                                   ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:73:39: Unsupported: ## (in sequence expression)
-   73 |   assert property (@(posedge clk) ##1 val |=> not val)
-      |                                       ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:76:35: Unsupported: ## () cycle delay range expression
-   76 |   assert property (@(posedge clk) ##1 (val) |=> not (val))
-      |                                   ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:76:40: Unsupported: ## (in sequence expression)
-   76 |   assert property (@(posedge clk) ##1 (val) |=> not (val))
-      |                                        ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:57: Unsupported: ## () cycle delay range expression
-   82 |   assert property (@(posedge clk) disable iff (cyc < 3) ##1 1 |=> cyc > 3)
-      |                                                         ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:61: Unsupported: ## (in sequence expression)
-   82 |   assert property (@(posedge clk) disable iff (cyc < 3) ##1 1 |=> cyc > 3)
-      |                                                             ^
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:85:36: Unsupported: ## () cycle delay range expression
-   85 |   assert property (@(posedge clk) (##1 val) |=> (##1 val))
-      |                                    ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:85:40: Unsupported: ## (in sequence expression)
-   85 |   assert property (@(posedge clk) (##1 val) |=> (##1 val))
-      |                                        ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:85:50: Unsupported: ## () cycle delay range expression
-   85 |   assert property (@(posedge clk) (##1 val) |=> (##1 val))
-      |                                                  ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:85:54: Unsupported: ## (in sequence expression)
-   85 |   assert property (@(posedge clk) (##1 val) |=> (##1 val))
-      |                                                      ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:103:14: Unsupported sequence match items
-  103 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
-      |              ^
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:103:29: Unsupported: ## range cycle delay range expression
-  103 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
-      |                             ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:103:39: Unsupported: ## (in sequence expression)
-  103 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
-      |                                       ^
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:102:13: Unsupported: property variable declaration
-  102 |     integer l_b;
-      |             ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:16: Unsupported sequence match items
-  120 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
-      |                ^
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:35: Unsupported: ## () cycle delay range expression
-  120 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
-      |                                   ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:51: Unsupported: [-> boolean abbrev expression
-  120 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
-      |                                                   ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:54: Unsupported: boolean abbrev (in sequence expression)
-  120 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
-      |                                                      ^
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:37: Unsupported: ## (in sequence expression)
-  120 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
-      |                                     ^
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:118:14: Unsupported: property variable declaration
-  118 |     realtime l_t;
-      |              ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:124:31: Unsupported: ## () cycle delay range expression
-  124 |   assert property (@clk not a ##1 b);
-      |                               ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:124:33: Unsupported: ## (in sequence expression)
-  124 |   assert property (@clk not a ##1 b);
-      |                                 ^
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:46:45: Unsupported: Implication with sequence expression
+   46 |   assert property (@(posedge clk) (##1 val) |-> (##1 val)) $display("[%0t] two delays implication stmt, fileline:%d", $time, 46);
+      |                                             ^~~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:48:52: Unsupported: Disable iff with sequence expression
+                                                    : ... note: In instance 't'
+   48 |   assert property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 48);
+      |                                                    ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:50:52: Unsupported: Disable iff with sequence expression
+                                                    : ... note: In instance 't'
+   50 |   assume property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 50);
+      |                                                    ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:51: Unsupported: Disable iff with sequence expression
+                                                    : ... note: In instance 't'
+   52 |   cover property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 52);
+      |                                                   ^~
 %Error: Exiting due to
diff --git a/test_regress/t/t_property_sexpr_unsup.v b/test_regress/t/t_property_sexpr_unsup.v
index 00379507a..91654e717 100644
--- a/test_regress/t/t_property_sexpr_unsup.v
+++ b/test_regress/t/t_property_sexpr_unsup.v
@@ -13,77 +13,44 @@ module t (  /*AUTOARG*/
   integer cyc = 1;
   bit val = 0;
 
-  Test test (  /*AUTOINST*/
-      // Inputs
-      .clk(clk),
-      .val(val),
-      .cyc(cyc)
-  );
-
   Ieee ieee();
 
   always @(posedge clk) begin
     if (cyc != 0) begin
       cyc <= cyc + 1;
       val = ~val;
-`ifdef TEST_VERBOSE
-      $display("cyc=%0d, val=%0d", cyc, val);
-`endif
       if (cyc == 10) begin
         $write("*-* All Finished *-*\n");
         $finish;
       end
     end
   end
-endmodule
+`ifdef PARSING_TIME
+  assert property (@(posedge clk) val ##1 val) $display("[%0t] var with single delay stmt, fileline:%d", $time, `__LINE__);
+  assert property (@(posedge clk) ##1 val ##2 val) $display("[%0t] sequence stmt, fileline:%d", $time, `__LINE__);
+`else
+  assert property (@(posedge clk) ##1 1 |-> 1) $display("[%0t] single delay with const implication stmt, fileline:%d", $time, `__LINE__);
 
-module Test (
-    input clk,
-    input bit val,
-    input integer cyc
-);
+  assert property (@(posedge clk) ##1 1 |-> not (val)) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, `__LINE__);
 
-  assert property (@(posedge clk) ##2 val)
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+  assert property (@(posedge clk) 1 |-> ##1 val) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, `__LINE__);
 
-  assert property (@(posedge clk) ##1 1 |=> 0)
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+  assert property (@(posedge clk) (##1 val) |-> (not val)) $display("[%0t] single delay with negated implication stmt, fileline:%d", $time, `__LINE__);
 
-  assert property (@(posedge clk) ##1 1 |=> not (val))
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+  assert property (@(posedge clk) ##1 (val) |-> not (val)) $display("[%0t] single delay with negated implication brackets stmt, fileline:%d", $time, `__LINE__);
 
-  assert property (@(posedge clk) ##1 val)
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+  assert property (@(posedge clk) ((val) |-> not (val))) $display("[%0t] disable iff with negated implication stmt, fileline:%d", $time, `__LINE__);
 
-  assert property (@(posedge clk) ##1 (val))
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+  assert property (@(posedge clk) ##1 1 |-> 0) $display("[%0t] disable iff with cond implication stmt, fileline:%d", $time, `__LINE__);
 
-  assert property (@(posedge clk) (##1 (val)))
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+  assert property (@(posedge clk) (##1 val) |-> (##1 val)) $display("[%0t] two delays implication stmt, fileline:%d", $time, `__LINE__);
 
-  assert property (@(posedge clk) (##1 (val)))
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+  assert property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__);
 
-  assert property (@(posedge clk) not (##1 val))
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+  assume property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__);
 
-  assert property (@(posedge clk) ##1 1 |=> 1)
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
-
-  assert property (@(posedge clk) ##1 val |=> not val)
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
-
-  assert property (@(posedge clk) ##1 (val) |=> not (val))
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
-
-  assert property (@(posedge clk) ((val) |=> not (val)))
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
-
-  assert property (@(posedge clk) disable iff (cyc < 3) ##1 1 |=> cyc > 3)
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
-
-  assert property (@(posedge clk) (##1 val) |=> (##1 val))
-  else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__);
+  cover property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__);
+`endif
 endmodule
 
 // Test parsing only
@@ -94,6 +61,7 @@ module Ieee;
   byte q[$];
   logic clk;
 
+`ifdef PARSING_TIME
   property p1;
     $rose(a) |-> q[0];
   endproperty
@@ -122,4 +90,5 @@ module Ieee;
 
   // IEEE 1800-2023 16.12.3
   assert property (@clk not a ##1 b);
+`endif
 endmodule
diff --git a/test_regress/t/t_sequence_first_match_unsup.out b/test_regress/t/t_sequence_first_match_unsup.out
new file mode 100644
index 000000000..2edc27797
--- /dev/null
+++ b/test_regress/t/t_sequence_first_match_unsup.out
@@ -0,0 +1,20 @@
+%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:47:40: Unsupported: or (in sequence expression)
+   47 |   initial p0: assert property ((##1 1) or (##2 1) |-> x==1);
+      |                                        ^~
+                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
+%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:50:52: Unsupported: or (in sequence expression)
+   50 |   initial p1: assert property (first_match((##1 1) or (##2 1)) |-> x==1);
+      |                                                    ^~
+%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:50:32: Unsupported: first_match (in sequence expression)
+   50 |   initial p1: assert property (first_match((##1 1) or (##2 1)) |-> x==1);
+      |                                ^~~~~~~~~~~
+%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:53:34: Unsupported: or (in sequence expression)
+   53 |   initial p2: assert property (1 or ##1 1 |-> x==0);
+      |                                  ^~
+%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:56:46: Unsupported: or (in sequence expression)
+   56 |   initial p3: assert property (first_match(1 or ##1 1) |-> x==0);
+      |                                              ^~
+%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:56:32: Unsupported: first_match (in sequence expression)
+   56 |   initial p3: assert property (first_match(1 or ##1 1) |-> x==0);
+      |                                ^~~~~~~~~~~
+%Error: Exiting due to
diff --git a/test_regress/t/t_sequence_first_match_unsup.py b/test_regress/t/t_sequence_first_match_unsup.py
new file mode 100755
index 000000000..26823c39a
--- /dev/null
+++ b/test_regress/t/t_sequence_first_match_unsup.py
@@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# Copyright 2025 by Wilson Snyder. This program is free software; you
+# can redistribute it and/or modify it under the terms of either the GNU
+# Lesser General Public License Version 3 or the Perl Artistic License
+# Version 2.0.
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('simulator')
+
+test.lint(expect_filename=test.golden_filename,
+          verilator_flags2=['--assert --error-limit 1000'],
+          fails=True)
+
+test.passes()
diff --git a/test_regress/t/t_sequence_first_match_unsup.v b/test_regress/t/t_sequence_first_match_unsup.v
new file mode 100644
index 000000000..e0dd187cd
--- /dev/null
+++ b/test_regress/t/t_sequence_first_match_unsup.v
@@ -0,0 +1,58 @@
+// (C) 2001-2020, Daniel Kroening, Edmund Clarke,
+// Computer Science Department, University of Oxford
+// Computer Science Department, Carnegie Mellon University
+//
+// All rights reserved. Redistribution and use in source and binary forms, with
+// or without modification, are permitted provided that the following
+// conditions are met:
+//
+//   1. Redistributions of source code must retain the above copyright
+//      notice, this list of conditions and the following disclaimer.
+//
+//   2. Redistributions in binary form must reproduce the above copyright
+//      notice, this list of conditions and the following disclaimer in the
+//      documentation and/or other materials provided with the distribution.
+//
+//   3. Neither the name of the University nor the names of its contributors
+//      may be used to endorse or promote products derived from this software
+//      without specific prior written permission.
+//
+// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
+// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+// POSSIBILITY OF SUCH DAMAGE.
+//
+// You can contact the author at:
+//   - homepage : https://www.cprover.org/ebmc/
+//   - source repository : https://github.com/diffblue/hw-cbmc
+
+module main(input clk);
+
+  reg [31:0] x = 0;
+
+  always @(posedge clk)
+    x<=x+1;
+
+  // Starting from a particular state,
+  // first_match yields the sequence that _ends_ first.
+
+  // fails
+  initial p0: assert property ((##1 1) or (##2 1) |-> x==1);
+
+  // passes
+  initial p1: assert property (first_match((##1 1) or (##2 1)) |-> x==1);
+
+  // fails
+  initial p2: assert property (1 or ##1 1 |-> x==0);
+
+  // passes
+  initial p3: assert property (first_match(1 or ##1 1) |-> x==0);
+
+endmodule
diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out
index 5a73a5851..1f9d09780 100644
--- a/test_regress/t/t_sequence_sexpr_unsup.out
+++ b/test_regress/t/t_sequence_sexpr_unsup.out
@@ -36,209 +36,182 @@
    52 |       a intersect b;
       |         ^~~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:55:4: Unsupported: sequence
-   55 |    sequence s_uni_cycdelay_int;
+   55 |    sequence s_uni_cycdelay_id;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:56:7: Unsupported: ## () cycle delay range expression
-   56 |       ## 1 b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:56:7: Unsupported: ## id cycle delay range expression
+   56 |       ## DELAY b;
       |       ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:56:12: Unsupported: ## (in sequence expression)
-   56 |       ## 1 b;
-      |            ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:58:4: Unsupported: sequence
-   58 |    sequence s_uni_cycdelay_id;
+   58 |    sequence s_uni_cycdelay_pid;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:59:7: Unsupported: ## id cycle delay range expression
-   59 |       ## DELAY b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:59:7: Unsupported: ## () cycle delay range expression
+   59 |       ## ( DELAY ) b;
       |       ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:59:16: Unsupported: ## (in sequence expression)
-   59 |       ## DELAY b;
-      |                ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:61:4: Unsupported: sequence
-   61 |    sequence s_uni_cycdelay_pid;
+   61 |    sequence s_uni_cycdelay_range;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:62:7: Unsupported: ## () cycle delay range expression
-   62 |       ## ( DELAY ) b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:62:7: Unsupported: ## range cycle delay range expression
+   62 |       ## [1:2] b;
       |       ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:62:20: Unsupported: ## (in sequence expression)
-   62 |       ## ( DELAY ) b;
-      |                    ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:64:4: Unsupported: sequence
-   64 |    sequence s_uni_cycdelay_range;
+   64 |    sequence s_uni_cycdelay_star;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:65:7: Unsupported: ## range cycle delay range expression
-   65 |       ## [1:2] b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:65:7: Unsupported: ## [*] cycle delay range expression
+   65 |       ## [*] b;
       |       ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:65:16: Unsupported: ## (in sequence expression)
-   65 |       ## [1:2] b;
-      |                ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:67:4: Unsupported: sequence
-   67 |    sequence s_uni_cycdelay_star;
+   67 |    sequence s_uni_cycdelay_plus;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:68:7: Unsupported: ## [*] cycle delay range expression
-   68 |       ## [*] b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:68:7: Unsupported: ## [+] cycle delay range expression
+   68 |       ## [+] b;
       |       ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:68:14: Unsupported: ## (in sequence expression)
-   68 |       ## [*] b;
-      |              ^
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:70:4: Unsupported: sequence
-   70 |    sequence s_uni_cycdelay_plus;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:71:4: Unsupported: sequence
+   71 |    sequence s_cycdelay_int;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:71:7: Unsupported: ## [+] cycle delay range expression
-   71 |       ## [+] b;
-      |       ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:71:14: Unsupported: ## (in sequence expression)
-   71 |       ## [+] b;
-      |              ^
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:74:4: Unsupported: sequence
-   74 |    sequence s_cycdelay_int;
-      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:75:9: Unsupported: ## () cycle delay range expression
-   75 |       a ## 1 b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:72:9: Unsupported: ## (in sequence expression)
+   72 |       a ## 1 b;
       |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:75:12: Unsupported: ## (in sequence expression)
-   75 |       a ## 1 b;
-      |            ^
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:77:4: Unsupported: sequence
-   77 |    sequence s_cycdelay_id;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:74:4: Unsupported: sequence
+   74 |    sequence s_cycdelay_id;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:78:9: Unsupported: ## id cycle delay range expression
-   78 |       a ## DELAY b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:75:9: Unsupported: ## id cycle delay range expression
+   75 |       a ## DELAY b;
+      |         ^~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:75:9: Unsupported: ## (in sequence expression)
+   75 |       a ## DELAY b;
+      |         ^~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:77:4: Unsupported: sequence
+   77 |    sequence s_cycdelay_pid;
+      |    ^~~~~~~~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:78:9: Unsupported: ## () cycle delay range expression
+   78 |       a ## ( DELAY ) b;
       |         ^~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:78:9: Unsupported: ## (in sequence expression)
-   78 |       a ## DELAY b;
+   78 |       a ## ( DELAY ) b;
       |         ^~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:80:4: Unsupported: sequence
-   80 |    sequence s_cycdelay_pid;
+   80 |    sequence s_cycdelay_range;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:81:9: Unsupported: ## () cycle delay range expression
-   81 |       a ## ( DELAY ) b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:81:9: Unsupported: ## range cycle delay range expression
+   81 |       a ## [1:2] b;
+      |         ^~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:81:9: Unsupported: ## (in sequence expression)
+   81 |       a ## [1:2] b;
       |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:81:14: Unsupported: ## (in sequence expression)
-   81 |       a ## ( DELAY ) b;
-      |              ^~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:83:4: Unsupported: sequence
-   83 |    sequence s_cycdelay_range;
+   83 |    sequence s_cycdelay_star;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:84:9: Unsupported: ## range cycle delay range expression
-   84 |       a ## [1:2] b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:84:9: Unsupported: ## [*] cycle delay range expression
+   84 |       a ## [*] b;
       |         ^~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:84:9: Unsupported: ## (in sequence expression)
-   84 |       a ## [1:2] b;
+   84 |       a ## [*] b;
       |         ^~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:86:4: Unsupported: sequence
-   86 |    sequence s_cycdelay_star;
+   86 |    sequence s_cycdelay_plus;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:87:9: Unsupported: ## [*] cycle delay range expression
-   87 |       a ## [*] b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:87:9: Unsupported: ## [+] cycle delay range expression
+   87 |       a ## [+] b;
       |         ^~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:87:9: Unsupported: ## (in sequence expression)
-   87 |       a ## [*] b;
+   87 |       a ## [+] b;
       |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:89:4: Unsupported: sequence
-   89 |    sequence s_cycdelay_plus;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:90:4: Unsupported: sequence
+   90 |    sequence s_booleanabbrev_brastar_int;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:90:9: Unsupported: ## [+] cycle delay range expression
-   90 |       a ## [+] b;
-      |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:90:9: Unsupported: ## (in sequence expression)
-   90 |       a ## [+] b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:91:9: Unsupported: [*] boolean abbrev expression
+   91 |       a [* 1 ];
       |         ^~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:91:12: Unsupported: boolean abbrev (in sequence expression)
+   91 |       a [* 1 ];
+      |            ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:93:4: Unsupported: sequence
-   93 |    sequence s_booleanabbrev_brastar_int;
+   93 |    sequence s_booleanabbrev_brastar;
       |    ^~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:9: Unsupported: [*] boolean abbrev expression
-   94 |       a [* 1 ];
+   94 |       a [*];
+      |         ^~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:9: Unsupported: boolean abbrev (in sequence expression)
+   94 |       a [*];
       |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:12: Unsupported: boolean abbrev (in sequence expression)
-   94 |       a [* 1 ];
-      |            ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:96:4: Unsupported: sequence
-   96 |    sequence s_booleanabbrev_brastar;
+   96 |    sequence s_booleanabbrev_plus;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:9: Unsupported: [*] boolean abbrev expression
-   97 |       a [*];
-      |         ^~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:9: Unsupported: [+] boolean abbrev expression
+   97 |       a [+];
+      |         ^~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:9: Unsupported: boolean abbrev (in sequence expression)
-   97 |       a [*];
-      |         ^~
+   97 |       a [+];
+      |         ^~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:99:4: Unsupported: sequence
-   99 |    sequence s_booleanabbrev_plus;
+   99 |    sequence s_booleanabbrev_eq;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:100:9: Unsupported: [+] boolean abbrev expression
-  100 |       a [+];
-      |         ^~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:100:9: Unsupported: boolean abbrev (in sequence expression)
-  100 |       a [+];
-      |         ^~~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:100:9: Unsupported: [= boolean abbrev expression
+  100 |       a [= 1];
+      |         ^~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:100:12: Unsupported: boolean abbrev (in sequence expression)
+  100 |       a [= 1];
+      |            ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:102:4: Unsupported: sequence
-  102 |    sequence s_booleanabbrev_eq;
+  102 |    sequence s_booleanabbrev_eq_range;
       |    ^~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:9: Unsupported: [= boolean abbrev expression
-  103 |       a [= 1];
+  103 |       a [= 1:2];
       |         ^~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:12: Unsupported: boolean abbrev (in sequence expression)
-  103 |       a [= 1];
+  103 |       a [= 1:2];
       |            ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:105:4: Unsupported: sequence
-  105 |    sequence s_booleanabbrev_eq_range;
+  105 |    sequence s_booleanabbrev_minusgt;
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:106:9: Unsupported: [= boolean abbrev expression
-  106 |       a [= 1:2];
-      |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:106:12: Unsupported: boolean abbrev (in sequence expression)
-  106 |       a [= 1:2];
-      |            ^
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:106:9: Unsupported: [-> boolean abbrev expression
+  106 |       a [-> 1];
+      |         ^~~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:106:13: Unsupported: boolean abbrev (in sequence expression)
+  106 |       a [-> 1];
+      |             ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:108:4: Unsupported: sequence
-  108 |    sequence s_booleanabbrev_minusgt;
+  108 |    sequence s_booleanabbrev_minusgt_range;
       |    ^~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:9: Unsupported: [-> boolean abbrev expression
-  109 |       a [-> 1];
+  109 |       a [-> 1:2];
       |         ^~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:13: Unsupported: boolean abbrev (in sequence expression)
-  109 |       a [-> 1];
+  109 |       a [-> 1:2];
       |             ^
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:111:4: Unsupported: sequence
-  111 |    sequence s_booleanabbrev_minusgt_range;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:112:4: Unsupported: sequence
+  112 |    sequence p_arg_seqence(sequence inseq);
       |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:112:9: Unsupported: [-> boolean abbrev expression
-  112 |       a [-> 1:2];
-      |         ^~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:112:13: Unsupported: boolean abbrev (in sequence expression)
-  112 |       a [-> 1:2];
-      |             ^
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:115:4: Unsupported: sequence
-  115 |    sequence p_arg_seqence(sequence inseq);
-      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:115:27: Unsupported: sequence argument data type
-  115 |    sequence p_arg_seqence(sequence inseq);
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:112:27: Unsupported: sequence argument data type
+  112 |    sequence p_arg_seqence(sequence inseq);
       |                           ^~~~~~~~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:116:4: Unsupported: sequence
+  116 |    sequence s_firstmatch_a;
+      |    ^~~~~~~~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:117:7: Unsupported: first_match (in sequence expression)
+  117 |       first_match (a);
+      |       ^~~~~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:119:4: Unsupported: sequence
-  119 |    sequence s_firstmatch_a;
+  119 |    sequence s_firstmatch_ab;
       |    ^~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:120:7: Unsupported: first_match (in sequence expression)
-  120 |       first_match (a);
+  120 |       first_match (a, res0 = 1);
       |       ^~~~~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:122:4: Unsupported: sequence
-  122 |    sequence s_firstmatch_ab;
+  122 |    sequence s_firstmatch_abc;
       |    ^~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:123:7: Unsupported: first_match (in sequence expression)
-  123 |       first_match (a, res0 = 1);
+  123 |       first_match (a, res0 = 1, res1 = 2);
       |       ^~~~~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:125:4: Unsupported: sequence
-  125 |    sequence s_firstmatch_abc;
-      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:126:7: Unsupported: first_match (in sequence expression)
-  126 |       first_match (a, res0 = 1, res1 = 2);
-      |       ^~~~~~~~~~~
-%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:129:10: Ignoring unsupported: cover sequence
-  129 |    cover sequence (s_a) $display("");
+%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:126:10: Ignoring unsupported: cover sequence
+  126 |    cover sequence (s_a) $display("");
       |          ^~~~~~~~
                    ... For warning description see https://verilator.org/warn/COVERIGN?v=latest
                    ... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message.
-%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:130:10: Ignoring unsupported: cover sequence
-  130 |    cover sequence (@(posedge a) disable iff (b) s_a) $display("");
+%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:127:10: Ignoring unsupported: cover sequence
+  127 |    cover sequence (@(posedge a) disable iff (b) s_a) $display("");
       |          ^~~~~~~~
-%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:131:10: Ignoring unsupported: cover sequence
-  131 |    cover sequence (disable iff (b) s_a) $display("");
+%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:128:10: Ignoring unsupported: cover sequence
+  128 |    cover sequence (disable iff (b) s_a) $display("");
       |          ^~~~~~~~
 %Error: Exiting due to
diff --git a/test_regress/t/t_sequence_sexpr_unsup.v b/test_regress/t/t_sequence_sexpr_unsup.v
index da3b99ec2..662f1f1c1 100644
--- a/test_regress/t/t_sequence_sexpr_unsup.v
+++ b/test_regress/t/t_sequence_sexpr_unsup.v
@@ -52,9 +52,6 @@ module t (/*AUTOARG*/
       a intersect b;
    endsequence
 
-   sequence s_uni_cycdelay_int;
-      ## 1 b;
-   endsequence
    sequence s_uni_cycdelay_id;
       ## DELAY b;
    endsequence