mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

missing break

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-31 01:59:39 -07:00
parent 0a1eba1a45
commit 9a64158e6e
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_parallel.cpp
View file

@ -207,13 +207,14 @@ namespace smt {
switch (r) {
case l_undef: {
replay_proof_prefixes();
break;
}
case l_true: {
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found formula sat\n");
model_ref mdl;
ctx->get_model(mdl);
b.set_sat(m_l2g, *mdl);
return;
break;
}
case l_false: {
expr_ref_vector const &unsat_core = ctx->unsat_core();
@ -221,7 +222,7 @@ namespace smt {
for (auto c : unsat_core) verbose_stream() << mk_bounded_pp(c, m, 3) << "\n");
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER determined formula unsat\n");
b.set_unsat(m_l2g, unsat_core);
return;
break;
}
}
}