mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
weird latent bug in wmax: init() succeeds and it returns undef
This commit is contained in:
parent
fdd5c923ed
commit
d8156aeff3
|
@ -213,7 +213,8 @@ namespace opt {
|
|||
try {
|
||||
is_sat = (*m_msolver)();
|
||||
}
|
||||
catch (z3_exception&) {
|
||||
catch (z3_exception& ex) {
|
||||
IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n");
|
||||
is_sat = l_undef;
|
||||
}
|
||||
if (is_sat != l_false) {
|
||||
|
|
|
@ -53,7 +53,7 @@ namespace opt {
|
|||
TRACE("opt", tout << "weighted maxsat\n";);
|
||||
scoped_ensure_theory wth(*this);
|
||||
reset();
|
||||
if (init())
|
||||
if (!init())
|
||||
return l_undef;
|
||||
|
||||
lbool is_sat = l_true;
|
||||
|
|
Loading…
Reference in a new issue