From a08c67685dec7ebb660d80b45db1f5802cd6ef15 Mon Sep 17 00:00:00 2001
From: Yilou Wang <wangyilou123@gmail.com>
Date: Tue, 3 Mar 2026 09:45:49 +0100
Subject: [PATCH] Fix bare variable constraint: wrap expr != 0 per IEEE 18.5.1

---
 src/V3Randomize.cpp | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp
index 762a7d93b..ac2776dc5 100644
--- a/src/V3Randomize.cpp
+++ b/src/V3Randomize.cpp
@@ -1900,6 +1900,20 @@ class ConstraintExprVisitor final : public VNVisitor {
     }
 
     void visit(AstConstraintExpr* nodep) override {
+        // IEEE 1800-2017 18.5.1: A bare expression used as a constraint is
+        // implicitly treated as "expr != 0" when wider than 1 bit.
+        // Must wrap before iterateChildren, which converts to SMT format.
+        {
+            AstNodeExpr* const exprp = nodep->exprp();
+            if (exprp->width() > 1) {
+                FileLine* const fl = exprp->fileline();
+                V3Number numZero{fl, exprp->width(), 0};
+                AstNodeExpr* const neqp
+                    = new AstNeq{fl, exprp->unlinkFrBack(), new AstConst{fl, numZero}};
+                neqp->user1(true);  // Mark as rand-dependent for SMT path
+                nodep->exprp(neqp);
+            }
+        }
         iterateChildren(nodep);
         if (m_wantSingle) {
             nodep->replaceWith(nodep->exprp()->unlinkFrBack());