search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

hea-use-after-free at ast.h:504 (caused by QF_NIA opt) #3561

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic QF_NIA)
(set-option :trace true)
(set-option :smt.bv.enable_int2bv true)
(declare-const v1 Bool)
(declare-const i0 Int)
(declare-const v15 Bool)
(declare-const i2 Int)
(assert (or (< (div (- (- (+ i0 i0)) (- (+ i0 i0)) (- (+ i0 i0)) (+ i0 i0) (- (+ i0 i0))) (abs (- (- (+ i0 i0)) (- (+ i0 i0)) (- (+ i0 i0)) (+ i0 i0) (- (+ i0 i0))))) 829)  (=> v15 (xor v1 (> i0 (- (+ i0 i0)))))))
(assert (or (> (abs (- (- (+ i0 i0)) (- (+ i0 i0)) (- (+ i0 i0)) (+ i0 i0) (- (+ i0 i0)))) i0)))
(minimize i2)
(check-sat)

z3 (commit 9be7bda) throws a heap-use-after-free

==82132==ERROR: AddressSanitizer: heap-use-after-free on address 0x6070001d890c at pc 0x000000467ad5 bp 0x7ffcc5941dd0 sp 0x7ffcc5941dc0                                                          [104/1536]
READ of size 4 at 0x6070001d890c thread T0
    #0 0x467ad4 in ast::get_kind() const ../src/ast/ast.h:504
    #1 0x467d7c in is_app(ast const*) ../src/ast/ast.h:914
    #2 0xbd3615 in get_depth(expr const*) ../src/ast/ast.h:1382
    #3 0xfcf5be in smt::context::internalize_deep(expr*) ../src/smt/smt_internalizer.cpp:188
    #4 0xfd1b01 in smt::context::internalize(expr*, bool) ../src/smt/smt_internalizer.cpp:338
    #5 0xe07ba0 in smt::theory_arith<smt::mi_ext>::branch_nl_int_var(int) ../src/smt/theory_arith_nl.h:812
    #6 0xe11af4 in smt::theory_arith<smt::mi_ext>::process_non_linear() ../src/smt/theory_arith_nl.h:2475
    #7 0xdcd054 in smt::theory_arith<smt::mi_ext>::final_check_core() ../src/smt/theory_arith_core.h:1488
    #8 0xdcd7b0 in smt::theory_arith<smt::mi_ext>::final_check_eh() ../src/smt/theory_arith_core.h:1526
    #9 0xf8c685 in smt::context::final_check() ../src/smt/smt_context.cpp:3908
    #10 0xf8b68e in smt::context::bounded_search() ../src/smt/smt_context.cpp:3824
    #11 0xf88dc9 in smt::context::search() ../src/smt/smt_context.cpp:3651
    #12 0xf867c4 in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3476
    #13 0xd04980 in smt::kernel::imp::setup_and_check() ../src/smt/smt_kernel.cpp:108
    #14 0xd0359b in smt::kernel::setup_and_check() ../src/smt/smt_kernel.cpp:292
    #15 0x5c528e in opt::opt_solver::check_sat_core2(unsigned int, expr* const*) ../src/opt/opt_solver.cpp:183
    #16 0x196435b in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #17 0x1968399 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #18 0x57b510 in opt::context::optimize(ref_vector<expr, ast_manager> const&) ../src/opt/opt_context.cpp:301
    #19 0x1920c81 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1557
    #20 0x18b0fc3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #21 0x18b4f5f in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #22 0x18b6671 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #23 0x1895656 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #24 0x43c0fe in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #25 0x453f92 in main ../src/shell/main.cpp:352
    #26 0x7f6e8fc5e82f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
NikolajBjorner commented 4 years ago

duplicate