From aad11271924960db1b84933481fc1eb60cd31d3f Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 23 Dec 2025 09:30:04 -0800
Subject: [PATCH] SMV: integer_number nonterminal

This adds the integer_number nonterminal rule, to match the NuSMV 2.7
manual.
---
 src/smvlang/parser.y | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index 04c54b741..3a0bd3d55 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -697,7 +697,9 @@ boolean_constant:
            }
            ;
 
-integer_constant:
+integer_constant: integer_number;
+
+integer_number:
              NUMBER_Token
            {
              init($$, ID_constant);
@@ -849,11 +851,11 @@ basic_expr : constant
            }
            ;
 
-bound      : '[' NUMBER_Token ',' NUMBER_Token ']'
+bound      : '[' integer_number ',' integer_number ']'
            { init($$); mto($$, $2); mto($$, $4); }
            ;
 
-range      : NUMBER_Token DOTDOT_Token NUMBER_Token
+range      : integer_number DOTDOT_Token integer_number
            { init($$); mto($$, $1); mto($$, $3); }
            ;