From df5c2adc4e79e32c47aabd1ccfb9cc674507d4f4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Dec 2013 15:39:38 -0600 Subject: [PATCH] debug opt Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 3 ++- src/tactic/arith/elim01_tactic.cpp | 19 ++++++++++--------- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 6501ef51b..6df46e783 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -92,7 +92,8 @@ namespace opt { case 1: return execute(m_objectives[0], false); default: { - symbol pri = m_params.get_sym("priority", symbol("lex")); + opt_params optp(m_params); + symbol pri = optp.priority(); if (pri == symbol("pareto")) { return execute_pareto(); } diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp index de76b5e62..af427ccc5 100644 --- a/src/tactic/arith/elim01_tactic.cpp +++ b/src/tactic/arith/elim01_tactic.cpp @@ -23,6 +23,7 @@ Notes: #include"expr_safe_replace.h" // NB: should use proof-producing expr_substitute in polished version. #include"arith_decl_plugin.h" #include"elim01_tactic.h" +#include"model_smt2_pp.h" class bool2int_model_converter : public model_converter { ast_manager& m; @@ -63,15 +64,15 @@ public: else { new_model->register_decl(f, fi); } - num = old_model->get_num_functions(); - for (unsigned i = 0; i < num; i++) { - func_decl * f = old_model->get_function(i); - func_interp * fi = old_model->get_func_interp(f); - new_model->register_decl(f, fi->copy()); - } - new_model->copy_usort_interps(*old_model); - old_model = new_model; - } + } + num = old_model->get_num_functions(); + for (unsigned i = 0; i < num; i++) { + func_decl * f = old_model->get_function(i); + func_interp * fi = old_model->get_func_interp(f); + new_model->register_decl(f, fi->copy()); + } + new_model->copy_usort_interps(*old_model); + old_model = new_model; } void insert(func_decl* x_new, func_decl* x_old) {