mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 17:45:32 +00:00
remove mc printing from goals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8b720a0d66
commit
ba79700096
2 changed files with 0 additions and 16 deletions
|
@ -188,10 +188,6 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
|
|||
}
|
||||
break;
|
||||
}
|
||||
if (m_mc && md) {
|
||||
// (*m_mc)(md);
|
||||
|
||||
}
|
||||
TRACE("tactic",
|
||||
if (m_mc) m_mc->display(tout << "mc:");
|
||||
if (g->mc()) g->mc()->display(tout << "g:");
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue