3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

add error generation for #4977

This commit is contained in:
Nikolaj Bjorner 2021-01-26 14:55:42 -08:00
parent 8ed1992029
commit e26e38b654

View file

@ -105,7 +105,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_optimize_maximize(c, o, t);
RESET_ERROR_CODE();
CHECK_VALID_AST(t,0);
CHECK_VALID_AST(t, 0);
CHECK_IS_EXPR(t, 0);
return to_optimize_ptr(o)->add_objective(to_app(t), true);
Z3_CATCH_RETURN(0);
}
@ -114,7 +115,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_optimize_minimize(c, o, t);
RESET_ERROR_CODE();
CHECK_VALID_AST(t,0);
CHECK_VALID_AST(t, 0);
CHECK_IS_EXPR(t, 0);
return to_optimize_ptr(o)->add_objective(to_app(t), false);
Z3_CATCH_RETURN(0);
}