diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index f1540d1b5..74cf974b2 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -2225,7 +2225,7 @@ struct
   let div (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_div ctx a b
 
   let neg (ctx:context) (a:rcf_num) = Z3native.rcf_neg ctx a
-  let inv (ctx:context) (a:rcf_num) = Z3native.rcf_neg ctx a
+  let inv (ctx:context) (a:rcf_num) = Z3native.rcf_inv ctx a
 
   let power (ctx:context) (a:rcf_num) (k:int) = Z3native.rcf_power ctx a k
 
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 86bb297e9..4453c94a7 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4371,6 +4371,8 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
             return BR_REWRITE_FULL;
     }
 
+#if 0
+    
     expr_ref hd(m()), tl(m());
     if (get_head_tail(a, hd, tl)) {
         //result = re().mk_in_re(tl, re().mk_derivative(hd, b));
@@ -4410,6 +4412,8 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
         return BR_REWRITE_FULL;
     }
 
+#endif
+
 #if 0
     unsigned len = 0;
     if (has_fixed_length_constraint(b, len)) {