mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
fixed problems with logger and invalid assertion
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
f0f90eecaa
commit
8191cc1951
|
@ -201,7 +201,7 @@ extern "C" {
|
|||
LOG_Z3_get_as_array_func_decl(c, a);
|
||||
RESET_ERROR_CODE();
|
||||
if (is_expr(to_ast(a)) && is_app_of(to_expr(a), mk_c(c)->get_array_fid(), OP_AS_ARRAY)) {
|
||||
return of_func_decl(to_func_decl(to_app(a)->get_decl()->get_parameter(0).get_ast()));
|
||||
RETURN_Z3(of_func_decl(to_func_decl(to_app(a)->get_decl()->get_parameter(0).get_ast())));
|
||||
}
|
||||
else {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
|
|
|
@ -58,7 +58,7 @@ namespace smt {
|
|||
\remark if negate == true, then the hypothesis is actually (not (= lhs rhs))
|
||||
*/
|
||||
proof * mk_hypothesis(ast_manager & m, app * eq, bool negate, expr * lhs, expr * rhs) {
|
||||
SASSERT(m.is_eq(eq));
|
||||
SASSERT(m.is_eq(eq) || m.is_iff(eq));
|
||||
SASSERT((eq->get_arg(0) == lhs && eq->get_arg(1) == rhs) ||
|
||||
(eq->get_arg(0) == rhs && eq->get_arg(1) == lhs));
|
||||
app * h = negate ? m.mk_not(eq) : eq;
|
||||
|
|
Loading…
Reference in a new issue