mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
throw exception instead of debug mode assertion in ast_manager on malformed input
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
parent
cd8f82ebc2
commit
c969d78042
|
@ -2043,7 +2043,15 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2
|
||||||
}
|
}
|
||||||
|
|
||||||
app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) {
|
app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) {
|
||||||
SASSERT(decl->get_arity() == num_args || decl->is_right_associative() || decl->is_left_associative() || decl->is_chainable());
|
if (decl->get_arity() != num_args &&
|
||||||
|
!decl->is_right_associative() &&
|
||||||
|
!decl->is_left_associative() &&
|
||||||
|
!decl->is_chainable()) {
|
||||||
|
std::ostringstream buffer;
|
||||||
|
buffer << "Wrong number of arguments (" << num_args
|
||||||
|
<< ") passed to function " << mk_pp(decl, *this);
|
||||||
|
throw ast_exception(buffer.str().c_str());
|
||||||
|
}
|
||||||
app * r = 0;
|
app * r = 0;
|
||||||
if (num_args > 2 && !decl->is_flat_associative()) {
|
if (num_args > 2 && !decl->is_flat_associative()) {
|
||||||
if (decl->is_right_associative()) {
|
if (decl->is_right_associative()) {
|
||||||
|
|
|
@ -717,7 +717,7 @@ struct euclidean_solver::imp {
|
||||||
elim_unit();
|
elim_unit();
|
||||||
else
|
else
|
||||||
decompose_and_elim();
|
decompose_and_elim();
|
||||||
TRACE("euclidean_solver_step", display(tout););
|
TRACE("euclidean_solver", display(tout););
|
||||||
if (inconsistent()) return false;
|
if (inconsistent()) return false;
|
||||||
}
|
}
|
||||||
return true;
|
return true;
|
||||||
|
|
|
@ -1041,8 +1041,8 @@ namespace smt {
|
||||||
num_args = 1;
|
num_args = 1;
|
||||||
args = &n;
|
args = &n;
|
||||||
}
|
}
|
||||||
for (unsigned j = 0; j < num_args; j++) {
|
for (unsigned i = 0; i < num_args; i++) {
|
||||||
expr * arg = args[j];
|
expr * arg = args[i];
|
||||||
expr * pp;
|
expr * pp;
|
||||||
rational a_val;
|
rational a_val;
|
||||||
get_monomial(arg, a_val, pp);
|
get_monomial(arg, a_val, pp);
|
||||||
|
|
Loading…
Reference in a new issue