1

Closed

(not foo xpto) crashes Z3

description

This line crashes Z3 (smtlib2 frontend):

(assert (and (not (>= 3 1) (= 1 2))))


Invalid read of size 4
at 0x8800FD3: ast_manager::coercion_needed(func_decl*, unsigned int, expr* const*)
by 0x8804C15: ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*)
by 0x88055E9: ast_manager::mk_app(func_decl*, unsigned int, expr* const*)
by 0x856610D: cmd_context::mk_app(symbol const&, unsigned int, ...) const
by 0x85505CE: smt2::parser::pop_app_frame(smt2::parser::app_frame*)
by 0x85559FB: smt2::parser::pop_expr_frame()
by 0x8555A6F: smt2::parser::parse_expr()
by 0x8555C71: smt2::parser::parse_assert()
Closed Nov 23, 2012 at 6:53 PM by leodemoura
Bug was fixed.

comments

leodemoura wrote Nov 23, 2012 at 6:53 PM

Thanks for reporting this bug.
I fixed it. The fix is already available in the contrib and unstable branches.

Thanks,
Leo