mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix bug exposed from relevancy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f0ef339623
commit
5566965a5a
|
@ -528,6 +528,9 @@ namespace smt {
|
|||
if (ctx.get_assignment(c.lit()) == l_undef) {
|
||||
return;
|
||||
}
|
||||
if (!ctx.is_relevant(c.lit())) {
|
||||
return;
|
||||
}
|
||||
numeral sum = numeral::zero(), maxsum = numeral::zero();
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
switch(ctx.get_assignment(c.lit(i))) {
|
||||
|
|
Loading…
Reference in a new issue