From b008d036dddc40d45b3b4c5723d94bc412980729 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 5 Nov 2013 17:38:50 -0800 Subject: [PATCH] trying to fix proof mode issue --- src/muz/duality/duality_dl_interface.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index eb74f797f..25dfcebbd 100644 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -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; @@ -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);