diff --git a/regression/ebmc/range_type/range_type7.desc b/regression/ebmc/range_type/range_type7.desc
new file mode 100644
index 00000000..5e4cb1bc
--- /dev/null
+++ b/regression/ebmc/range_type/range_type7.desc
@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+range_type7.smv
+--bound 5
+^\[spec1\] G x != 1: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
diff --git a/regression/ebmc/range_type/range_type7.smv b/regression/ebmc/range_type/range_type7.smv
new file mode 100644
index 00000000..b6eb3181
--- /dev/null
+++ b/regression/ebmc/range_type/range_type7.smv
@@ -0,0 +1,14 @@
+MODULE main
+VAR x:1..6;
+
+ASSIGN
+  init(x) := 6;
+
+  next(x) :=
+    case
+      x!=1 : x - 1;
+      TRUE: 1;
+    esac;
+
+-- should fail
+LTLSPEC G x!=1
diff --git a/regression/ebmc/range_type/range_type8.desc b/regression/ebmc/range_type/range_type8.desc
new file mode 100644
index 00000000..8d55f699
--- /dev/null
+++ b/regression/ebmc/range_type/range_type8.desc
@@ -0,0 +1,9 @@
+KNOWNBUG broken-smt-backend
+range_type8.smv
+--bound 5
+^\[spec1\] G x != 1: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+We do not have type checking for unary minus.
diff --git a/regression/ebmc/range_type/range_type8.smv b/regression/ebmc/range_type/range_type8.smv
new file mode 100644
index 00000000..ad15b99d
--- /dev/null
+++ b/regression/ebmc/range_type/range_type8.smv
@@ -0,0 +1,14 @@
+MODULE main
+VAR x:1..6;
+
+ASSIGN
+  init(x) := 6;
+
+  next(x) :=
+    case
+      x!=1 : x + -1; -- unary minus
+      TRUE: 1;
+    esac;
+
+-- should fail
+LTLSPEC G x!=1