mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

fix #4176

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-01 16:34:33 -07:00
parent c94a9e8ddd
commit 6088da5159
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_setup.cpp
View file

@ -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() {
@ -682,7 +683,6 @@ namespace smt {
//
setup_mi_arith();
setup_arrays();
setup_card();
}
void setup::setup_UFNIA() {
@ -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();
}
@ -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();

4
src/tactic/tactic.cpp
View file

@ -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()