Closed muchang closed 3 weeks ago
[548] % z3release small.smt2 Segmentation fault [549] % z3debug small.smt2 unsat [550] % z3san small.smt2 AddressSanitizer:DEADLYSIGNAL ================================================================= ==2397280==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000001 (pc 0x560f5965ae7f bp 0x7ffddb8ea6a0 sp 0x7ffddb8ea6a0 T0) ==2397280==The signal is caused by a READ memory access. ==2397280==Hint: address points to the zero page. #0 0x560f5965ae7f in ast_table::push_erase(ast*) ../src/ast/ast.cpp:572 #1 0x560f5966b824 in ast_manager::delete_node(ast*) ../src/ast/ast.cpp:1804 #2 0x560f587fcc57 in ast_manager::dec_ref(ast*) ../src/ast/ast.h:1654 #3 0x560f587fcc57 in obj_ref<expr, ast_manager>::dec_ref() ../src/util/obj_ref.h:32 #4 0x560f587fcc57 in obj_ref<expr, ast_manager>::~obj_ref() ../src/util/obj_ref.h:59 #5 0x560f587fcc57 in seq_rewriter::mk_antimirov_deriv_concat(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:3427 #6 0x560f5881490e in seq_rewriter::mk_antimirov_deriv_rec(expr*, expr*, expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:3351 #7 0x560f58816b48 in seq_rewriter::mk_antimirov_deriv(expr*, expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:3194 #8 0x560f5881f6ad in seq_rewriter::mk_str_in_regexp(expr*, expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:4557 #9 0x560f5883f31c in seq_rewriter::mk_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:706 #10 0x560f58a45d36 in reduce_app_core ../src/ast/rewriter/th_rewriter.cpp:226 #11 0x560f58a45d36 in reduce_app ../src/ast/rewriter/th_rewriter.cpp:627 #12 0x560f58a4e61c in process_app<false> ../src/ast/rewriter/rewriter_def.h:316 #13 0x560f58a4e61c in resume_core<false> ../src/ast/rewriter/rewriter_def.h:783 #14 0x560f58a4e61c in main_loop<false> ../src/ast/rewriter/rewriter_def.h:742 #15 0x560f58a4e61c in operator() ../src/ast/rewriter/rewriter_def.h:822 #16 0x560f58a5a741 in th_rewriter::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/th_rewriter.cpp:1011 #17 0x560f5756a064 in asserted_formulas::assert_expr(expr*, app*) ../src/solver/assertions/asserted_formulas.cpp:170 #18 0x560f567359c7 in smt::context::assert_expr_core(expr*, app*) ../src/smt/smt_context.cpp:3029 #19 0x560f567359c7 in smt::context::assert_expr_core(expr*, app*) ../src/smt/smt_context.cpp:3021 #20 0x560f567359c7 in smt::context::assert_expr(expr*, app*) ../src/smt/smt_context.cpp:3045 #21 0x560f567359c7 in smt::context::assert_expr(expr*) ../src/smt/smt_context.cpp:3040 #22 0x560f57d8dee5 in solver::assert_expr(expr*) ../src/solver/solver.cpp:205 #23 0x560f57d8dee5 in solver::assert_expr(expr*) ../src/solver/solver.cpp:205 #24 0x560f57c8aa58 in cmd_context::assert_expr(expr*) ../src/cmd_context/cmd_context.cpp:1550 #25 0x560f57c4debc in smt2::parser::parse_assert() ../src/parsers/smt2/smt2parser.cpp:2608 #26 0x560f57c590d7 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2961 #27 0x560f57c590d7 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3191 #28 0x560f57c04ffd in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3242 #29 0x560f54ea7411 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:182 #30 0x560f54e7c992 in main ../src/shell/main.cpp:384 #31 0x7fb7cff01d8f (/lib/x86_64-linux-gnu/libc.so.6+0x29d8f) #32 0x7fb7cff01e3f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x29e3f) #33 0x560f54e97ac4 in _start (/local/home/suz/suz-local/software/z3san/build-06062024081119-49610f5/z3+0x7b0ac4) AddressSanitizer can not provide additional info. SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.cpp:572 in ast_table::push_erase(ast*) ==2397280==ABORTING [551] % cat small.smt2 (assert (str.in_re "0" ((_ re.loop 0 1) ((_ re.loop 0 1) (str.to_re "1"))))) (check-sat)
Changing one or both of the 1's in the two re.loop's to another constant makes the segfault disappear.
version: 35c1cac
Changing one or both of the 1's in the two re.loop's to another constant makes the segfault disappear.
version: 35c1cac