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)