From 71b6a493d6aefda738d78ce17bec7ee3598453b3 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 10 Dec 2025 14:19:28 -0800
Subject: [PATCH] SMV: error mod and div on integers

We do not have backend support for mod and div on integers.  Hence, print an
error message.
---
 regression/smv/expressions/div1.desc |  6 +++---
 regression/smv/expressions/mod1.desc |  6 +++---
 src/smvlang/smv_typecheck.cpp        | 10 ++++++++--
 3 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/regression/smv/expressions/div1.desc b/regression/smv/expressions/div1.desc
index 67968ae6c..a3e08692c 100644
--- a/regression/smv/expressions/div1.desc
+++ b/regression/smv/expressions/div1.desc
@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 div1.smv
 
-^EXIT=0$
+^file .* line 4: no support for / on integer operands$
+^EXIT=2$
 ^SIGNAL=0$
 --
 --
-div is not implemented.
diff --git a/regression/smv/expressions/mod1.desc b/regression/smv/expressions/mod1.desc
index 2e6e4a620..13a26b69f 100644
--- a/regression/smv/expressions/mod1.desc
+++ b/regression/smv/expressions/mod1.desc
@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 mod1.smv
 
-^EXIT=0$
+^file .* line 4: no support for % on integer operands$
+^EXIT=2$
 ^SIGNAL=0$
 --
 --
-mod is not implemented.
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index d996f3f37..0eedb41ff 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -806,9 +806,15 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
       else if(expr.id() == ID_mult)
         new_range = smv_range0 * smv_range1;
       else if(expr.id() == ID_div)
-        new_range = smv_range0;
+      {
+        throw errort().with_location(expr.source_location())
+          << "no support for / on integer operands";
+      }
       else if(expr.id() == ID_mod)
-        new_range = smv_range1;
+      {
+        throw errort().with_location(expr.source_location())
+          << "no support for % on integer operands";
+      }
       else
         assert(false);