From 1137d237251bf334bfc38b6c3652180f7b24d5c3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Mar 2026 23:20:16 -0700 Subject: [PATCH] fix bug reported in API coherence report Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 2 +- src/ast/rewriter/seq_rewriter.cpp | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) 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)) {