SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

Memory leak on integer formula #310

Closed rainoftime closed 3 years ago

rainoftime commented 3 years ago

Hi, for the following formula

(set-logic QF_IDL)
(declare-const i0 Int)
(declare-const i3 Int)
(assert (distinct (- 0 i0) i3))
(check-sat)

yices 5019920

(error "formula is not in integer difference logic")

=================================================================
==8443==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 1600 byte(s) in 1 object(s) allocated from:
    #0 0x7f4b810ae662 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98662)
    #1 0x71a7af in safe_malloc utils/memalloc.c:62
    #2 0x5700a6 in init_smt_core solvers/cdcl/smt_core.c:1564
    #3 0x44d00e in init_solvers context/context.c:5458
    #4 0x44de03 in init_context context/context.c:5627
    #5 0x421c70 in _o_yices_create_context api/yices_api.c:8286
    #6 0x421cca in yices_create_context api/yices_api.c:8293
    #7 0x7fb0f1 in init_smt2_context frontend/smt2/smt2_commands.c:2604
    #8 0x7fd16f in check_delayed_assertions frontend/smt2/smt2_commands.c:3044
    #9 0x80bc51 in smt2_check_sat frontend/smt2/smt2_commands.c:6640
    #10 0x81b061 in eval_smt2_check_sat frontend/smt2/smt2_term_stack.c:1052
    #11 0x4ee2ae in tstack_eval parser_utils/term_stack2.c:5445
    #12 0x8123ea in smt2_parse frontend/smt2/smt2_parser.c:316
    #13 0x813b25 in parse_smt2_command frontend/smt2/smt2_parser.c:960
    #14 0x40a085 in main frontend/yices_smt2.c:1094
    #15 0x7f4b804a783f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2083f)
BrunoDutertre commented 3 years ago

Fixed in dcea185e7617089b0103013700c9a3a8992d1bc3.