mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

trying to fix proof mode issue

Browse source
This commit is contained in:
Ken McMillan 2013-11-05 17:38:50 -08:00
parent fa05116e66
commit b008d036dd
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/muz/duality/duality_dl_interface.cpp
View file

@ -35,6 +35,7 @@ Revision History:
#include "model_smt2_pp.h"
#include "model_v2_pp.h"
#include "fixedpoint_params.hpp"
#include "scoped_proof.h"
// template class symbol_table<family_id>;
@ -82,7 +83,7 @@ dl_interface::dl_interface(datalog::context& dl_ctx) :
{
_d = 0;
dl_ctx.get_manager().toggle_proof_mode(PGM_FINE);
// dl_ctx.get_manager().toggle_proof_mode(PGM_FINE);
}
@ -131,6 +132,8 @@ lbool dl_interface::query(::expr * query) {
if(old_data)
old_cex = old_data->cex;
scoped_proof generate_proofs_please(m_ctx.get_manager());
// make a new problem and solver
_d = alloc(duality_data,m_ctx.get_manager());
_d->ls = alloc(RPFP::iZ3LogicSolver,_d->ctx);