diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 75c0d9daf..e8d07498f 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4006,12 +4006,16 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const*
         np = f->get_num_parameters();
         lo2 = np > 0 ? f->get_parameter(0).get_int() : 0;
         hi2 = np > 1 ? f->get_parameter(1).get_int() : lo2;
-        // (loop a 0 0) = ""
-        if  (np == 2 && lo2 > hi2) {
+        if  (np == 2 && (lo2 > hi2 || hi2 < 0)) {
             result = re().mk_empty(args[0]->get_sort());
             return BR_DONE;
         }
-        if (np == 2 && hi2 == 0) {
+        if (np == 1 && lo2 < 0) {
+            result = re().mk_empty(args[0]->get_sort());
+            return BR_DONE;
+        }
+        // (loop a 0 0) = ""
+        if (np == 2 && lo2 == 0 && hi2 == 0) {
             result = re().mk_to_re(str().mk_empty(re().to_seq(args[0]->get_sort())));
             return BR_DONE;
         }
@@ -4041,6 +4045,10 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const*
             result = re().mk_loop(args[0], n1.get_unsigned());
             return BR_REWRITE1;
         }
+        if (m_autil.is_numeral(args[1], n1) && n1 < 0) {
+            result = re().mk_empty(args[0]->get_sort());
+            return BR_DONE;
+        }
         break;
     case 3:
         if (m_autil.is_numeral(args[1], n1) && n1.is_unsigned() &&