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

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-28 21:51:51 -08:00
parent 8ea49eed8e
commit 4ffe3fab05
2 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifiers/model_reconstruction_trail.cpp
View file

@ -69,7 +69,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
args.push_back(m.mk_var(i, d->get_domain(i)));
head = m.mk_app(d, args);
mrp.insert(head, def, dep);
TRACE("simplifier", tout << d << " " << def << " " << dep << "\n");
TRACE("simplifier", tout << mk_pp(d, m) << " " << mk_pp(def,m) << " " << "\n");
dependent_expr de(m, def, nullptr, dep);
add_vars(de, free_vars);
}

1
src/ast/simplifiers/reduce_args_simplifier.cpp
View file

@ -328,7 +328,6 @@ class reduce_args_simplifier : public dependent_expr_simplifier {
ptr_buffer<expr> new_args;
var_ref_vector new_vars(m);
ptr_buffer<expr> new_eqs;
generic_model_converter * f_mc = alloc(generic_model_converter, m, "reduce_args");
for (auto const& [f, map] : decl2arg2funcs)
for (auto const& [t, new_def] : *map)
m_fmls.model_trail().hide(new_def);