mirror of
https://github.com/Z3Prover/z3
synced 2025-04-16 13:58:45 +00:00
parent
a2aab76c22
commit
0f566ddf38
|
@ -1079,7 +1079,9 @@ namespace qe {
|
|||
TRACE("qe", tout << "component of core is not true: " << mk_pp(c, m) << "\n";
|
||||
tout << mdl << "\n";
|
||||
);
|
||||
return false;
|
||||
if (mdl.is_false(c)) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
return true;
|
||||
|
|
Loading…
Reference in a new issue