mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

use safe replace for external substitution

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-24 18:47:19 +03:00
parent 1b8d1a1ccc
commit 4363c9f44f
1 changed files with 3 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/api/api_ast.cpp
View file

@ -31,7 +31,7 @@ Revision History:
#include"ast_smt2_pp.h" #include"ast_smt2_pp.h"
#include"th_rewriter.h" #include"th_rewriter.h"
#include"var_subst.h" #include"var_subst.h"
#include"expr_substitution.h" #include"expr_safe_replace.h"
#include"pp.h" #include"pp.h"
#include"scoped_ctrl_c.h" #include"scoped_ctrl_c.h"
#include"cancel_eh.h" #include"cancel_eh.h"
@ -786,17 +786,12 @@ extern "C" {
RETURN_Z3(of_expr(0)); RETURN_Z3(of_expr(0));
} }
} }
expr_safe_replace subst(m);
expr_substitution subst(m);
for (unsigned i = 0; i < num_exprs; i++) { for (unsigned i = 0; i < num_exprs; i++) {
subst.insert(from[i], to[i]); subst.insert(from[i], to[i]);
} }
th_rewriter m_rw(m);
m_rw.set_substitution(&subst);
expr_ref new_a(m); expr_ref new_a(m);
proof_ref pr(m); subst(a, new_a);
m_rw(a, new_a, pr);
mk_c(c)->save_ast_trail(new_a); mk_c(c)->save_ast_trail(new_a);
r = new_a.get(); r = new_a.get();
RETURN_Z3(of_expr(r)); RETURN_Z3(of_expr(r));