mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove exit
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a4f2a1bb2e
commit
30e0f78c16
|
@ -207,7 +207,7 @@ br_status array_rewriter::mk_select_same_store(unsigned num_args, expr * const *
|
|||
result = std::move(tmp); \
|
||||
return status; \
|
||||
} \
|
||||
goto exit
|
||||
return BR_FAILED;
|
||||
|
||||
while (true) {
|
||||
if (m_util.is_store(arg0)) {
|
||||
|
@ -228,8 +228,8 @@ br_status array_rewriter::mk_select_same_store(unsigned num_args, expr * const *
|
|||
result = to_app(arg0)->get_arg(num_args);
|
||||
first = false;
|
||||
}
|
||||
else if (result != to_app(arg0)->get_arg(num_args))
|
||||
goto exit;
|
||||
else if (result != to_app(arg0)->get_arg(num_args))
|
||||
return BR_FAILED;
|
||||
arg0 = to_app(arg0)->get_arg(0);
|
||||
continue;
|
||||
}
|
||||
|
@ -278,8 +278,6 @@ br_status array_rewriter::mk_select_same_store(unsigned num_args, expr * const *
|
|||
}
|
||||
break;
|
||||
}
|
||||
|
||||
exit:
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue