From b129ee764fda0d33fdf94b487e0c265a3a308e6c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 20 Jan 2018 10:20:22 -0800
Subject: [PATCH] debugging opt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/pdecl.cpp              | 3 +++
 src/sat/sat_solver/inc_sat_solver.cpp  | 5 ++++-
 src/tactic/generic_model_converter.cpp | 2 --
 3 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 7eac1f347..7a85e87a2 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -866,6 +866,7 @@ psort * pdecl_manager::mk_psort_cnst(sort * s) {
 }
 
 psort * pdecl_manager::register_psort(psort * n) {
+    enable_trace("register_psort");
     TRACE("register_psort", tout << "registering psort...\n"; n->display(tout); tout << "\n";);
     psort * r = m_table.insert_if_not_there(n);
     if (r != n) {
@@ -946,6 +947,8 @@ void pdecl_manager::del_decl_core(pdecl * p) {
 }
 
 void pdecl_manager::del_decl(pdecl * p) {
+enable_trace("register_psort");
+    TRACE("register_psort", tout << "del psort "; p->display(tout); tout << "\n";);   
     if (p->is_psort()) {
         psort * _p = static_cast<psort*>(p);
         if (_p->is_sort_wrapper())
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index f0d945d59..0ad665c5e 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -830,7 +830,7 @@ private:
 
         // IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "after\n"););
 
-#if 0
+#if 1
         IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";);
         model_evaluator eval(*m_model);
         for (expr * f : m_fmls) {
@@ -842,6 +842,9 @@ private:
             if (!m.is_true(tmp)) {
                 IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n";);
                 IF_VERBOSE(0, verbose_stream() << m_params << "\n";);
+                IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "sat mc\n"););
+                IF_VERBOSE(0, if (m_mc0) m_mc0->display(verbose_stream() << "mc0\n"););
+                break;
             }
             VERIFY(m.is_true(tmp));                                
         }
diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp
index 4f48c78e1..139355d5f 100644
--- a/src/tactic/generic_model_converter.cpp
+++ b/src/tactic/generic_model_converter.cpp
@@ -89,9 +89,7 @@ void generic_model_converter::operator()(model_ref & md) {
 }
 
 void generic_model_converter::display(std::ostream & out) {
-    unsigned i = 0;
     for (entry const& e : m_entries) {
-        ++i;
         switch (e.m_instruction) {
         case instruction::HIDE:
             display_del(out, e.m_f);