From ea16c2f57970fe1d96c2d7ae7fb51838e7ef38fa Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 17 Oct 2025 08:42:33 -0700
Subject: [PATCH] SMV: tests for mod and div

The tests for mod and div on integers are KNOWNBUG; the ones for bit-vectors
work.
---
 regression/smv/expressions/div1.desc | 8 ++++++++
 regression/smv/expressions/div1.smv  | 7 +++++++
 regression/smv/expressions/mod1.desc | 8 ++++++++
 regression/smv/expressions/mod1.smv  | 7 +++++++
 regression/smv/word/div1.desc        | 6 ++++++
 regression/smv/word/div1.smv         | 7 +++++++
 regression/smv/word/mod1.desc        | 6 ++++++
 regression/smv/word/mod1.smv         | 7 +++++++
 8 files changed, 56 insertions(+)
 create mode 100644 regression/smv/expressions/div1.desc
 create mode 100644 regression/smv/expressions/div1.smv
 create mode 100644 regression/smv/expressions/mod1.desc
 create mode 100644 regression/smv/expressions/mod1.smv
 create mode 100644 regression/smv/word/div1.desc
 create mode 100644 regression/smv/word/div1.smv
 create mode 100644 regression/smv/word/mod1.desc
 create mode 100644 regression/smv/word/mod1.smv

diff --git a/regression/smv/expressions/div1.desc b/regression/smv/expressions/div1.desc
new file mode 100644
index 000000000..67968ae6c
--- /dev/null
+++ b/regression/smv/expressions/div1.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+div1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+div is not implemented.
diff --git a/regression/smv/expressions/div1.smv b/regression/smv/expressions/div1.smv
new file mode 100644
index 000000000..19e759fe2
--- /dev/null
+++ b/regression/smv/expressions/div1.smv
@@ -0,0 +1,7 @@
+MODULE main
+
+-- NuSMV 2.7 manual page 16
+CTLSPEC 7/5 = 1
+CTLSPEC -7/5 = -1
+CTLSPEC 7/-5 = -1
+CTLSPEC -7/-5 = 1
diff --git a/regression/smv/expressions/mod1.desc b/regression/smv/expressions/mod1.desc
new file mode 100644
index 000000000..2e6e4a620
--- /dev/null
+++ b/regression/smv/expressions/mod1.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+mod1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+mod is not implemented.
diff --git a/regression/smv/expressions/mod1.smv b/regression/smv/expressions/mod1.smv
new file mode 100644
index 000000000..5e18bf792
--- /dev/null
+++ b/regression/smv/expressions/mod1.smv
@@ -0,0 +1,7 @@
+MODULE main
+
+-- NuSMV 2.7 manual page 16
+CTLSPEC 7 mod 5 = 2
+CTLSPEC -7 mod 5 = -2
+CTLSPEC 7 mod -5 = 2
+CTLSPEC -7 mod -5 = -2
diff --git a/regression/smv/word/div1.desc b/regression/smv/word/div1.desc
new file mode 100644
index 000000000..107e92db7
--- /dev/null
+++ b/regression/smv/word/div1.desc
@@ -0,0 +1,6 @@
+CORE
+div1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/smv/word/div1.smv b/regression/smv/word/div1.smv
new file mode 100644
index 000000000..38c49dbe3
--- /dev/null
+++ b/regression/smv/word/div1.smv
@@ -0,0 +1,7 @@
+MODULE main
+
+-- bit-vector version of NuSMV 2.7 manual page 16
+CTLSPEC swconst(7, 8)/swconst(5, 8) = swconst(1, 8)
+CTLSPEC swconst(-7, 8)/swconst(5, 8) = swconst(-1, 8)
+CTLSPEC swconst(7, 8)/swconst(-5, 8) = swconst(-1, 8)
+CTLSPEC swconst(-7, 8)/swconst(-5, 8) = swconst(1, 8)
diff --git a/regression/smv/word/mod1.desc b/regression/smv/word/mod1.desc
new file mode 100644
index 000000000..de2c23ef3
--- /dev/null
+++ b/regression/smv/word/mod1.desc
@@ -0,0 +1,6 @@
+CORE
+mod1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/smv/word/mod1.smv b/regression/smv/word/mod1.smv
new file mode 100644
index 000000000..99990dffd
--- /dev/null
+++ b/regression/smv/word/mod1.smv
@@ -0,0 +1,7 @@
+MODULE main
+
+-- bit-vector version of NuSMV 2.7 manual page 16
+CTLSPEC swconst(7, 8) mod swconst(5, 8) = swconst(2, 8)
+CTLSPEC swconst(-7, 8) mod swconst(5, 8) = swconst(-2, 8)
+CTLSPEC swconst(7, 8) mod swconst(-5, 8) = swconst(2, 8)
+CTLSPEC swconst(-7, 8) mod swconst(-5, 8) = swconst(-2, 8)