allow range comparison for bit-vectors and int/real

src/ast/char_decl_plugin.cpp

@@ -16,6 +16,7 @@ Module Name:
 
 --*/
 #include "util/gparams.h"
+#include "ast/bv_decl_plugin.h"
 #include "ast/char_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_pp.h"
@@ -164,6 +165,14 @@ app* char_decl_plugin::mk_le(expr* a, expr* b) {
     unsigned v1 = 0, v2 = 0;
     if (a == b)
         return m_manager->mk_true();
+    bv_util bv(*m_manager);
+    if (bv.is_bv(a)) 
+        return bv.mk_ule(a, b);
+    arith_util arith(*m_manager);
+    if (arith.is_int_real(a))
+        return arith.mk_le(a, b);
+    if (a->get_sort() != char_sort()) 
+        throw default_exception("range comparison is only supported for bit-vectors, int, real and characters");
     bool c1 = is_const_char(a, v1);
     bool c2 = is_const_char(b, v2);
     if (c1 && c2)

src/ast/rewriter/seq_rewriter.cpp

@@ -3128,8 +3128,8 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
         expr_ref range(m());
         expr_ref psi(m().mk_false(), m());
         if (str().is_unit_string(r1, c1) && str().is_unit_string(r2, c2)) {
-            SASSERT(u().is_char(c1));
-            SASSERT(u().is_char(c2));
+            // SASSERT(u().is_char(c1));
+            // SASSERT(u().is_char(c2));
             // case: c1 <= e <= c2
             range = simplify_path(e, m().mk_and(u().mk_le(c1, e), u().mk_le(e, c2)));
             psi = simplify_path(e, m().mk_and(path, range));