mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
d3db2af81d
commit
299a6f4aee
|
@ -282,11 +282,13 @@ class horn_tactic : public tactic {
|
|||
}
|
||||
case l_false: {
|
||||
// goal is sat
|
||||
mc = concat(g->mc(), mc.get());
|
||||
g->reset();
|
||||
if (produce_models) {
|
||||
model_ref md = m_ctx.get_model();
|
||||
model_converter_ref mc2 = model2model_converter(md.get());
|
||||
mc = concat(mc.get(), mc2.get());
|
||||
TRACE("dl", mc->display(tout << *md << "\n"););
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
|
|
@ -95,6 +95,7 @@ public:
|
|||
g->inc_depth();
|
||||
}
|
||||
result.push_back(g.get());
|
||||
CTRACE("invertible_tactic", g->mc(), g->mc()->display(tout););
|
||||
}
|
||||
|
||||
void cleanup() override {}
|
||||
|
|
Loading…
Reference in a new issue