Merge pull request #1330 from diffblue/smv-mod1

tautschnig · web-flow · commit 68b2bb05a93f · 2025-10-18T09:27:30.000+02:00
SMV: tests for mod and div
diff --git a/regression/smv/expressions/div1.desc 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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)
