search

SRI-CSL / yices2

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

Segment fault in mcsat_process_registeration_queue #400

Closed merlinsun closed 5 months ago

merlinsun commented 2 years ago

Hi, for this instance, yices2 https://github.com/SRI-CSL/yices2/commit/09f162107cc9140172e6c890d8ccc633126c3720 yields Segmentation fault.

$ yices_smt2 delta.smt2 --incremental --mcsat
Segmentation fault (core dumped)
$ yices_smt2_asan delta.smt2 --incremental --mcsat
ASAN:DEADLYSIGNAL
=================================================================
==10592==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x560038edc581 bp 0x000000000000 sp 0x7ffde1b1d410 T0)
==10592==The signal is caused by a READ memory access.
==10592==Hint: address points to the zero page.
    #0 0x560038edc580 in mcsat_process_registeration_queue (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x53c580)
    #1 0x560038edcded in mcsat_assert_formula (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x53cded)
    #2 0x560038eef525 in mcsat_assert_formulas (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x54f525)
    #3 0x560038a45774 in context_process_assertions (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0xa5774)
    #4 0x560038a499cd in assert_formula (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0xa99cd)
    #5 0x560038fcf0cd in smt2_assert (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x62f0cd)
    #6 0x560038fe6f80 in eval_smt2_assert (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x646f80)
    #7 0x560038fda77c in smt2_parse.constprop.6 (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x63a77c)
    #8 0x5600389e9079 in main (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x49079)
    #9 0x7faf5296ec86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)
    #10 0x5600389ee1e9 in _start (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x4e1e9)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x53c580) in mcsat_process_registeration_queue
==10592==ABORTING
$ cat delta.smt2 
(set-logic ALL)
(declare-fun b ((Array Int (Array Int Real)) Int) Bool)
(declare-fun v () (Array Int (Array Int Real)))
(assert (or (b v 0)))
dddejan commented 2 years ago

The MCSAT solver does not support arrays. This is an issue with error handling and reporting.

merlinsun commented 2 years ago

I'm sorry for that. But the combination of bv and arithmetic also seems to make yices error. I'm not sure if it is valuable.

$ cat case.smt2
(set-logic ALL)
(declare-fun v () (_ BitVec 1))
(declare-fun a () Int)
(assert (distinct (= 0 a) (= v (_ bv1 1))))
(check-sat)
$ yices2 case.smt2 --incremental --mcsat
ASAN:DEADLYSIGNAL
=================================================================
==44000==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x55d2348615da bp 0x0fff964e400e sp 0x7ffcb2720000 T0)
==44000==The signal is caused by a READ memory access.
==44000==Hint: address points to the zero page.
    #0 0x55d2348615d9 in bv_evaluator_run_atom (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x5b45d9)
    #1 0x55d2348628a9 in bv_evaluator_run_term.part.18 (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x5b58a9)
    #2 0x55d234860f27 in bv_evaluator_run_atom (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x5b3f27)
    #3 0x55d234865b8b in bv_evaluator_evaluate_var (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x5b8b8b)
    #4 0x55d23484ee7a in bv_plugin_propagate (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x5a1e7a)
    #5 0x55d2347e5407 in mcsat_propagate (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x538407)
    #6 0x55d2347f820e in mcsat_solve (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x54b20e)
    #7 0x55d23437163e in check_context (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0xc463e)
    #8 0x55d2348dd042 in smt2_check_sat (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x630042)
    #9 0x55d2348f3ef8 in eval_smt2_check_sat (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x646ef8)
    #10 0x55d2348e777c in smt2_parse.constprop.6 (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x63a77c)
    #11 0x55d2342f6079 in main (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x49079)
    #12 0x7f64edb4ec86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)
    #13 0x55d2342fb1e9 in _start (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x4e1e9)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (/root/yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2+0x5b45d9) in bv_evaluator_run_atom
==44000==ABORTING