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

fix #3118 (without breaking #3101, #3111)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-09 21:20:27 +01:00
parent f7747d9e76
commit a51d65d58a
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/solver/tactic2solver.cpp
View file

@ -194,7 +194,9 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
if (g->mc()) g->mc()->display(tout << "g:"); if (g->mc()) g->mc()->display(tout << "g:");
if (md) tout << *md.get() << "\n"; if (md) tout << *md.get() << "\n";
); );
if (m_mc && md) {
(*m_mc)(md);
}
m_mc = concat(g->mc(), m_mc.get()); m_mc = concat(g->mc(), m_mc.get());
} }