Skip to content

Commit

Permalink
fix #4176
Browse files Browse the repository at this point in the history
  • Loading branch information
NikolajBjorner committed May 1, 2020
1 parent c94a9e8 commit 6088da5
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
4 changes: 1 addition & 3 deletions src/smt/smt_setup.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,7 @@ namespace smt {
case CFG_LOGIC: setup_default(); break;
case CFG_AUTO: setup_auto_config(); break;
}
setup_card();
}

void setup::setup_default() {
Expand Down Expand Up @@ -682,7 +683,6 @@ namespace smt {
//
setup_mi_arith();
setup_arrays();
setup_card();
}

void setup::setup_UFNIA() {
Expand Down Expand Up @@ -957,7 +957,6 @@ namespace smt {
setup_recfuns();
setup_dl();
setup_seq_str(st);
setup_card();
setup_fpa();
if (st.m_has_sr) setup_special_relations();
}
Expand All @@ -973,7 +972,6 @@ namespace smt {
setup_bv();
setup_dl();
setup_seq_str(st);
setup_card();
setup_fpa();
setup_recfuns();
if (st.m_has_sr) setup_special_relations();
Expand Down
4 changes: 3 additions & 1 deletion src/tactic/tactic.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,9 @@ struct tactic_report::imp {
~imp() {
m_watch.stop();
double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
TRACE("tactic", m_goal.display(tout););
TRACE("tactic", m_goal.display(tout << m_id << "\n");
if (m_goal.mc()) m_goal.mc()->display(tout);
);
IF_VERBOSE(0,
verbose_stream() << "(" << m_id
<< " :num-exprs " << m_goal.num_exprs()
Expand Down

0 comments on commit 6088da5

Please sign in to comment.