diff --git a/regression/cbmc-library/strtol-02/test.desc b/regression/cbmc-library/strtol-02/test.desc
index 9efefbc7362..92776cb5537 100644
--- a/regression/cbmc-library/strtol-02/test.desc
+++ b/regression/cbmc-library/strtol-02/test.desc
@@ -1,8 +1,11 @@
 CORE
 main.c
-
+--signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+Even with --signed-overflow-check enabled, verification should succeed here as
+strtol reports overflow condition with errno set to ERANGE.
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index 64664c44e8b..ca0c5e8dd33 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -353,9 +353,15 @@ inline long strtol(const char *nptr, char **endptr, int base)
       break;
 
     in_number=1;
-    long res_before=res;
-    res=res*base+ch-sub;
-    if(res<res_before)
+    _Bool overflow = __CPROVER_overflow_mult(res, (long)base);
+#pragma CPROVER check push
+#pragma CPROVER check disable "signed-overflow"
+    // This is now safe; still do it within the scope of the pragma to avoid an
+    // unnecessary assertion to be generated.
+    if(!overflow)
+      res *= base;
+#pragma CPROVER check pop
+    if(overflow || __CPROVER_overflow_plus(res, (long)(ch - sub)))
     {
       errno=ERANGE;
       if(sign=='-')
@@ -363,6 +369,7 @@ inline long strtol(const char *nptr, char **endptr, int base)
       else
         return LONG_MAX;
     }
+    res += ch - sub;
   }
 
   if(endptr!=0)