mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-08 00:05:46 +00:00
Code Activity

remove passing proof parameter to expr-inverter

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-25 11:15:09 -08:00
parent f100d2f4de
commit b3de7ac595
3 changed files with 10 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -63,7 +63,6 @@ void elim_unconstrained::eliminate() {
while (!m_heap.empty()) {
expr_ref r(m);
proof_ref pr(m);
int v = m_heap.erase_min();
node& n = get_node(v);
if (n.m_refcount == 0)
@ -85,7 +84,7 @@ void elim_unconstrained::eliminate() {
unsigned sz = m_args.size();
for (expr* arg : *to_app(t))
m_args.push_back(reconstruct_term(get_node(arg)));
bool inverted = m_inverter(t->get_decl(), to_app(t)->get_num_args(), m_args.data() + sz, r, pr);
bool inverted = m_inverter(t->get_decl(), to_app(t)->get_num_args(), m_args.data() + sz, r);
n.m_refcount = 0;
m_args.shrink(sz);
if (!inverted) {
@ -114,7 +113,6 @@ void elim_unconstrained::eliminate() {
IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(get_node(v).m_orig, m) << " " << mk_bounded_pp(t, m) << " -> " << r << " " << get_node(e).m_refcount << "\n";);
SASSERT(!pr && "not implemented to add proofs\n");
}
}