issues on QF_BVFP formulas

[zhendongsu]

Spurious error, solution unsoundness, or invalid model:

[539] % z3release model_validate=true small.smt2
sat
(error "line 2 column 163: invalid extract application")
sat
(error "line 3 column 10: an invalid model was generated")
[540] % cat small.smt2
(check-sat)
(assert (and false (= (_ bv0 32) (bvor ((_ extract 31 0) ((_ sign_extend 2) ((_ fp.to_sbv 32) RTZ (fp (_ bv0 1) (_ bv2047 11) (_ bv1 52))))) (concat (_ bv0 32))))))
(check-sat)

[zhendongsu]

[546] % z3release model_validate=true small.smt2
(error "line 9 column 46: invalid extract application")
Segmentation fault
[547] % z3san small.smt2
(error "line 9 column 46: invalid extract application")
=================================================================
==10339==ERROR: AddressSanitizer: heap-use-after-free on address 0x603000000013 at pc 0x55eeb5f3322c bp 0x7ffc2d30e5e0 sp 0x7ffc2d30e5d0
READ of size 2 at 0x603000000013 thread T0
    #0 0x55eeb5f3322b in func_decl_info::is_right_associative() const ../src/ast/ast.h:407
    #1 0x55eeb5f3322b in func_decl::is_right_associative() const ../src/ast/ast.h:647
    #2 0x55eeb5f3322b in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2244
    #3 0x55eeb514d3de in ast_manager::mk_app(func_decl*, expr*) ../src/ast/ast.h:1872
    #4 0x55eeb514d3de in mk_extract_proc::operator()(unsigned int, unsigned int, expr*) ../src/ast/rewriter/mk_extract_proc.cpp:45
    #5 0x55eeb503f440 in bv_rewriter::mk_sign_extend(unsigned int, expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/bv_rewriter.cpp:1612
    #6 0x55eeb4fb6ea3 in reduce_app_core ../src/ast/rewriter/th_rewriter.cpp:235
    #7 0x55eeb4fb6ea3 in reduce_app ../src/ast/rewriter/th_rewriter.cpp:648
    #8 0x55eeb4fc925c in process_app<false> ../src/ast/rewriter/rewriter_def.h:316
    #9 0x55eeb4fc925c in resume_core<false> ../src/ast/rewriter/rewriter_def.h:787
    #10 0x55eeb4fc925c in main_loop<false> ../src/ast/rewriter/rewriter_def.h:746
    #11 0x55eeb4fc925c in operator() ../src/ast/rewriter/rewriter_def.h:826
    #12 0x55eeb3de113b in asserted_formulas::assert_expr(expr*, app*) ../src/solver/assertions/asserted_formulas.cpp:167
    #13 0x55eeb3251a57 in smt::context::assert_expr_core(expr*, app*) ../src/smt/smt_context.cpp:3024
    #14 0x55eeb3251a57 in smt::context::assert_expr(expr*, app*) ../src/smt/smt_context.cpp:3036
    #15 0x55eeb3251a57 in smt::context::assert_expr(expr*) ../src/smt/smt_context.cpp:3031
    #16 0x55eeb47289d3 in solver::assert_expr(expr*) ../src/solver/solver.cpp:205
    #17 0x55eeb47289d3 in solver::assert_expr(expr*) ../src/solver/solver.cpp:205
    #18 0x55eeb4688f94 in cmd_context::assert_expr(expr*) ../src/cmd_context/cmd_context.cpp:1474
    #19 0x55eeb45ea131 in smt2::parser::parse_assert() ../src/parsers/smt2/smt2parser.cpp:2586
    #20 0x55eeb45f50f7 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2941
    #21 0x55eeb45f50f7 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3166
    #22 0x55eeb45aa1c5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3217
    #23 0x55eeb16bec01 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:144
    #24 0x55eeb1692861 in main ../src/shell/main.cpp:381
    #25 0x7f788c86bc86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)
    #26 0x55eeb169f8d9 in _start (/local/suz-local/software/z3san/build-12042022095531-9b58135/z3+0x20a8d9)

0x603000000013 is located 3 bytes inside of 24-byte region [0x603000000010,0x603000000028)
freed by thread T0 here:
    #0 0x7f788d877f30 in realloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdef30)
    #1 0x55eeb64ecc41 in memory::reallocate(void*, unsigned long) ../src/util/memory_manager.cpp:334
    #2 0x55eeb64afe41 in vector<unsigned long, false, unsigned int>::expand_vector() ../src/util/vector.h:202
    #3 0x55eeb64afe41 in vector<unsigned long, false, unsigned int>::push_back(unsigned long const&) ../src/util/vector.h:523
    #4 0x55eeb64afe41 in prime_generator::process_next_k_numbers(unsigned long) ../src/util/prime_generator.cpp:63
    #5 0x55eeb64b1218 in prime_generator::initialize() ../src/util/prime_generator.cpp:80
    #6 0x55eeb64b1218 in prime_iterator::initialize() ../src/util/prime_generator.cpp:133
    #7 0x55eeb1723c58 in mem_initialize() ../src/shell/mem_initializer.cpp:11
    #8 0x55eeb64ebd21 in memory::initialize(unsigned long) ../src/util/memory_manager.cpp:117
    #9 0x55eeb1692091 in main ../src/shell/main.cpp:334
    #10 0x7f788c86bc86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)

previously allocated by thread T0 here:
    #0 0x7f788d877b40 in __interceptor_malloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdeb40)
    #1 0x55eeb64ecb7d in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:301
    #2 0x55eeb64b13d1 in vector<unsigned long, false, unsigned int>::expand_vector() ../src/util/vector.h:183
    #3 0x55eeb64b13d1 in vector<unsigned long, false, unsigned int>::push_back(unsigned long&&) ../src/util/vector.h:539
    #4 0x55eeb64b13d1 in prime_generator::initialize() ../src/util/prime_generator.cpp:78
    #5 0x55eeb64b13d1 in prime_iterator::initialize() ../src/util/prime_generator.cpp:133
    #6 0x55eeb1723c58 in mem_initialize() ../src/shell/mem_initializer.cpp:11
    #7 0x55eeb64ebd21 in memory::initialize(unsigned long) ../src/util/memory_manager.cpp:117
    #8 0x55eeb1692091 in main ../src/shell/main.cpp:334
    #9 0x7f788c86bc86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)

SUMMARY: AddressSanitizer: heap-use-after-free ../src/ast/ast.h:407 in func_decl_info::is_right_associative() const
Shadow bytes around the buggy address:
  0x0c067fff7fb0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x0c067fff7fc0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x0c067fff7fd0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x0c067fff7fe0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x0c067fff7ff0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
=>0x0c067fff8000: fa fa[fd]fd fd fa fa fa fd fd fd fa fa fa fd fd
  0x0c067fff8010: fd fd fa fa fd fd fd fd fa fa 00 00 00 00 fa fa
  0x0c067fff8020: 00 00 00 00 fa fa 00 00 00 00 fa fa 00 00 00 fa
  0x0c067fff8030: fa fa 00 00 00 fa fa fa 00 00 00 fa fa fa 00 00
  0x0c067fff8040: 00 fa fa fa 00 00 00 fa fa fa 00 00 00 fa fa fa
  0x0c067fff8050: 00 00 00 fa fa fa 00 00 00 fa fa fa 00 00 00 fa
Shadow byte legend (one shadow byte represents 8 application bytes):
  Addressable:           00
  Partially addressable: 01 02 03 04 05 06 07 
  Heap left redzone:       fa
  Freed heap region:       fd
  Stack left redzone:      f1
  Stack mid redzone:       f2
  Stack right redzone:     f3
  Stack after return:      f5
  Stack use after scope:   f8
  Global redzone:          f9
  Global init order:       f6
  Poisoned by user:        f7
  Container overflow:      fc
  Array cookie:            ac
  Intra object redzone:    bb
  ASan internal:           fe
  Left alloca redzone:     ca
  Right alloca redzone:    cb
==10339==ABORTING
[548] % 
[548] % cat small.smt2
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (let ((qb (concat (select a (_ bv2 32)) (concat (select a (_
  bv1 32)) (select a (_ bv0 32)))))) (let ((qc (concat (select a (_
  bv5 32)) (concat (select a (_ bv4 32)) (concat (select a (_ bv3 32))
  qb))))) (let ((qd ((_ to_fp 11 53) (concat (select a (_ bv7 32))
  (concat (select a (_ bv6 32)) qc))))) (let ((qg ((_ sign_extend 2)
  ((_ fp.to_sbv 32) roundTowardZero (fp.abs qd)))) (qe ((_ extract 31
  0) (concat (_ bv0 32))))) (let ((qf (bvudiv ((_ extract 31 0) qg) (_
  bv10 32)))) (= (_ bv0 32) (bvor qf qe))))))))
(assert (let ((qb (concat (select a (_ bv2 32)) (concat (select a (_
  bv1 32)) (select a (_ bv0 32)))))) (let ((qc (concat (select a (_
  bv5 32)) (concat (select a (_ bv4 32)) (concat (select a (_ bv3 32))
  qb))))) (let ((qd ((_ to_fp 11 53) (concat (select a (_ bv7 32))
  (concat (select a (_ bv6 32)) qc))))) (let ((qg ((_ sign_extend 32)
  ((_ fp.to_sbv 32) roundTowardZero (fp.neg qd))))) (let ((qe ((_
  extract 1 0) (concat ((_ extract 63 32) qg))))) (distinct qe)))))))
(check-sat)