mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

build fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-08-28 18:43:50 -07:00
parent 8b8caf9ded
commit 4d29925c3f
3 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast_pp_util.h
View file

@ -38,7 +38,7 @@ class ast_pp_util {
decl_collector coll;
ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), coll(m), m_defined(m) {}
ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), m_defined(m), coll(m) {}
void reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u);
m_is_defined.reset(); m_defined.reset(); m_defined_lim.reset(); }

8
src/sat/smt/arith_diagnostics.cpp
View file

@ -162,14 +162,14 @@ namespace arith {
args.push_back(s.literal2expr(lit));
}
for (unsigned i = m_eq_head; i < m_eq_tail; ++i) {
auto const& [a, b, is_eq] = a.m_arith_hint.eq(i);
expr_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m);
auto const& [x, y, is_eq] = a.m_arith_hint.eq(i);
expr_ref eq(m.mk_eq(x->get_expr(), y->get_expr()), m);
if (!is_eq) eq = m.mk_not(eq);
args.push_back(arith.mk_int(lc));
args.push_back(eq);
}
for (expr* a : args)
sorts.push_back(a->get_sort());
for (expr* arg : args)
sorts.push_back(arg->get_sort());
sort* range = m.mk_proof_sort();
func_decl* d = m.mk_func_decl(symbol(name), args.size(), sorts.data(), range);
expr* r = m.mk_app(d, args);