mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
trying to figure out address dependency
This commit is contained in:
parent
ac9a7748e8
commit
bb61f17989
|
@ -513,6 +513,7 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
|
|||
opts.set("weak","1");
|
||||
|
||||
::ast *proof = m_solver->get_proof();
|
||||
show_assertion_ids();
|
||||
iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts);
|
||||
|
||||
std::vector<expr> linearized_interpolants(_interpolants.size());
|
||||
|
@ -613,6 +614,14 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
|
|||
pp.display_smt2(std::cout, m_solver->get_assertion(n-1));
|
||||
}
|
||||
|
||||
void solver::show_assertion_ids() {
|
||||
unsigned n = m_solver->get_num_assertions();
|
||||
std::cerr << "assertion ids: ";
|
||||
for (unsigned i = 0; i < n-1; ++i)
|
||||
std::cerr << " " << m_solver->get_assertion(i)->get_id();
|
||||
std::cerr << "\n";
|
||||
}
|
||||
|
||||
void include_ast_show(ast &a){
|
||||
a.show();
|
||||
}
|
||||
|
|
|
@ -907,6 +907,7 @@ namespace Duality {
|
|||
unsigned get_scope_level(){return m_solver->get_scope_level();}
|
||||
|
||||
void show();
|
||||
void show_assertion_ids();
|
||||
|
||||
proof get_proof(){
|
||||
return proof(ctx(),m_solver->get_proof());
|
||||
|
|
Loading…
Reference in a new issue