mirror of
https://github.com/Z3Prover/z3
synced 2025-07-17 09:56:39 +00:00
remove case with hi = 0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f8d328b1fb
commit
9d6c870e97
1 changed files with 0 additions and 3 deletions
|
@ -2024,9 +2024,6 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
|
||||||
if (lo == 0) {
|
if (lo == 0) {
|
||||||
return expr_ref(m().mk_true(), m());
|
return expr_ref(m().mk_true(), m());
|
||||||
}
|
}
|
||||||
else if (hi == 0) {
|
|
||||||
return expr_ref(m().mk_false(), m());
|
|
||||||
}
|
|
||||||
else {
|
else {
|
||||||
return is_nullable(r1);
|
return is_nullable(r1);
|
||||||
}
|
}
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue