mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

changing model format in duality to support boogie

Browse source
This commit is contained in:
Ken McMillan 2013-05-31 18:00:50 -07:00
parent ca38158966
commit 9890b3bb5c
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz_qe/duality_dl_interface.cpp
View file

@ -307,7 +307,7 @@ void dl_interface::display_certificate(std::ostream& out) {
local_func_decls = &locals;
print_proof(this,out,_d->cex);
out << ")\n";
out << "(model \n";
out << "(model \n\"";
::model mod(m_ctx.get_manager());
model orig_model = _d->cex.tree->dualModel;
for(unsigned i = 0; i < orig_model.num_consts(); i++){
@ -325,7 +325,7 @@ void dl_interface::display_certificate(std::ostream& out) {
}
}
model_v2_pp(out,mod);
out << ")\n";
out << "\")\n";
}
}