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);