From c387863da1d9d1465d147a1ba14d487294ddd7d5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 15 Feb 2021 14:14:25 -0800
Subject: [PATCH] fix #5032, reset substitution during fold transformation

---
 src/ast/ast.h                  | 6 ++++++
 src/ast/recfun_decl_plugin.cpp | 4 +++-
 src/smt/theory_char.cpp        | 2 +-
 3 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/ast/ast.h b/src/ast/ast.h
index f3b813fb0..def06f906 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -2453,6 +2453,12 @@ typedef obj_ref<app, ast_manager>        app_ref;
 typedef obj_ref<var,ast_manager>         var_ref;
 typedef app_ref proof_ref;
 
+inline expr_ref operator~(expr_ref const & e) {
+    if (e.m().is_not(e))
+        return expr_ref(to_app(e)->get_arg(0), e.m());
+    return expr_ref(e.m().mk_not(e), e.m());
+}
+
 // -----------------------------------
 //
 // ast_vector (smart pointer vector)
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index 5c670c126..43455437f 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -496,6 +496,7 @@ namespace recfun {
                 if (max_score <= 4) 
                     break;
 
+
                 ptr_vector<sort> domain;
                 ptr_vector<expr> args;
                 for (unsigned i = 0; i < n; ++i) {
@@ -508,9 +509,10 @@ namespace recfun {
                 func_decl* f = pd.get_def()->get_decl();
                 expr_ref new_body(m().mk_app(f, n, args.c_ptr()), m());
                 set_definition(subst, pd, n, vars, max_expr);
+                subst.reset();
                 subst.insert(max_expr, new_body);
                 result = subst(result);                
-                TRACEFN("substituted\n" << mk_pp(max_expr, m()) << "\n->\n" << new_body << "\n" << result);
+                TRACEFN("substituted\n" << mk_pp(max_expr, m()) << "\n->\n" << new_body << "\n-result->\n" << result);
             }
             return result;
         }
diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp
index 5b17e7ed2..f32f99714 100644
--- a/src/smt/theory_char.cpp
+++ b/src/smt/theory_char.cpp
@@ -258,7 +258,7 @@ namespace smt {
         for (unsigned v = get_num_vars(); v-- > 0; ) {
             expr* e = get_expr(v);
             if (seq.is_char(e) && m_var2value[v] == UINT_MAX && get_char_value(v, c)) {
-                CTRACE("seq", seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << get_char_value(v, c) << "\n";);
+                CTRACE("seq_verbose", seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << get_char_value(v, c) << "\n";);
                 enode* r = get_enode(v)->get_root();
                 m_value2var.reserve(c + 1, null_theory_var);
                 theory_var u = m_value2var[c];