fix bugs found while running sample from #1112 in debug mode

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_solver.cpp

@@ -17,6 +17,11 @@ Revision History:
 
 --*/
 #include<iostream>
+#include "util/scoped_ctrl_c.h"
+#include "util/cancel_eh.h"
+#include "util/file_path.h"
+#include "util/scoped_timer.h"
+#include "ast/ast_pp.h"
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
@@ -26,14 +31,10 @@ Revision History:
 #include "api/api_stats.h"
 #include "api/api_ast_vector.h"
 #include "solver/tactic2solver.h"
-#include "util/scoped_ctrl_c.h"
-#include "util/cancel_eh.h"
-#include "util/file_path.h"
-#include "util/scoped_timer.h"
+#include "solver/smt_logics.h"
 #include "tactic/portfolio/smt_strategic_solver.h"
 #include "smt/smt_solver.h"
 #include "smt/smt_implied_equalities.h"
-#include "solver/smt_logics.h"
 #include "cmd_context/cmd_context.h"
 #include "parsers/smt2/smt2parser.h"
 #include "sat/dimacs.h"

src/cmd_context/cmd_context.cpp

@@ -719,6 +719,7 @@ void cmd_context::init_manager_core(bool new_manager) {
     m_dt_eh = alloc(dt_eh, *this);
     m_pmanager->set_new_datatype_eh(m_dt_eh.get());
     if (!has_logic()) {
+        TRACE("cmd_context", tout << "init manager\n";);
         // add list type only if the logic is not specified.
         // it prevents clashes with builtin types.
         insert(pm().mk_plist_decl());
@@ -1408,7 +1409,8 @@ void cmd_context::restore_assertions(unsigned old_sz) {
         SASSERT(m_assertions.empty());
         return;
     }
-    SASSERT(old_sz <= m_assertions.size());
+    if (old_sz == m_assertions.size()) return;
+    SASSERT(old_sz < m_assertions.size());
     SASSERT(!m_interactive_mode || m_assertions.size() == m_assertion_strings.size());
     restore(m(), m_assertions, old_sz);
     if (produce_unsat_cores())

src/cmd_context/pdecl.cpp

@@ -852,7 +852,7 @@ pdecl_manager::pdecl_manager(ast_manager & m):
 pdecl_manager::~pdecl_manager() {
     dec_ref(m_list);
     reset_sort_info();
-    SASSERT(m_sort2psort.empty());    
+    SASSERT(m_sort2psort.empty());
     SASSERT(m_table.empty());
 }
 
@@ -946,6 +946,7 @@ void pdecl_manager::del_decl_core(pdecl * p) {
 }
 
 void pdecl_manager::del_decl(pdecl * p) {
+    TRACE("pdecl_manager", p->display(tout); tout << "\n";);
     if (p->is_psort()) {
         psort * _p = static_cast<psort*>(p);
         if (_p->is_sort_wrapper())

src/smt/smt_context.cpp

@@ -3143,6 +3143,7 @@ namespace smt {
             push_scope();
             for (unsigned i = 0; i < num_assumptions; i++) {
                 expr * curr_assumption = assumptions[i];
+                if (m_manager.is_true(curr_assumption)) continue;
                 SASSERT(is_valid_assumption(m_manager, curr_assumption));
                 proof * pr = m_manager.mk_asserted(curr_assumption);
                 internalize_assertion(curr_assumption, pr, 0);

src/solver/combined_solver.cpp

@@ -18,10 +18,11 @@ Author:
 Notes:
 
 --*/
-#include "solver/solver.h"
 #include "util/scoped_timer.h"
-#include "solver/combined_solver_params.hpp"
 #include "util/common_msgs.h"
+#include "ast/ast_pp.h"
+#include "solver/solver.h"
+#include "solver/combined_solver_params.hpp"
 #define PS_VB_LVL 15
 
 /**