search

Z3Prover / z3

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

heap-use-after-free at math/polynomial/algebraic_numbers.h:371:40 #6971

Closed merlinsun closed 11 months ago

merlinsun commented 11 months ago

Hi, For this instance, z3 https://github.com/Z3Prover/z3/commit/938a89e197549d67f7e804fe1d395a03037b4a3e 

$ cat small.smt2 
(declare-const x Bool)
(declare-const x1 Bool)
(declare-const x8 Bool)
(declare-fun a () Real)
(declare-fun va () Real)
(declare-fun r4 () Real)
(declare-fun r1 () Real)
(declare-fun r3 () Int)
(declare-fun ar3 () Real)
(declare-fun r () Real)
(declare-fun r2 () Real)
(declare-fun ar () Real)
(declare-fun r31 () Real)
(declare-fun r36 () Int)
(declare-fun r43 () Real)
(declare-fun v () Real)
(assert (or (and x8 x x1 (> v (/ ar va))) (and x8 (< 0.0 r43) (< r4 (/ r31 r31)) (= 1 (* r43 r43 3)) (= (/ 1 4) (+ r3 1 (* r36 a)))) (and (< va ar3) (not (and (= (+ 1.0 (* r1 r2)) r) (= a 0.0))))))
(check-sat-using smt)
$ z3asan small.smt2          
=================================================================
==12690==ERROR: AddressSanitizer: heap-use-after-free on address 0x613000047020 at pc 0x0000048cf491 bp 0x7ffdb1cc9020 sp 0x7ffdb1cc9018
READ of size 8 at 0x613000047020 thread T0
    #0 0x48cf490 in algebraic_numbers::anum::is_basic() const /root/z3/build/../src/math/polynomial/algebraic_numbers.h:371:40
    #1 0x48c6810 in algebraic_numbers::manager::imp::compare(algebraic_numbers::anum&, algebraic_numbers::anum&) /root/z3/build/../src/math/polynomial/algebraic_numbers.cpp:1950:19
    #2 0x48c6944 in algebraic_numbers::manager::imp::eq(algebraic_numbers::anum&, algebraic_numbers::anum&) /root/z3/build/../src/math/polynomial/algebraic_numbers.cpp:1965:20
    #3 0x48b3e6c in algebraic_numbers::manager::eq(algebraic_numbers::anum const&, algebraic_numbers::anum const&) /root/z3/build/../src/math/polynomial/algebraic_numbers.cpp:3045:23
    #4 0x24c3b03 in smt::theory_lra::imp::is_eq(int, int) /root/z3/build/../src/smt/theory_lra.cpp:1607:32
    #5 0x24c76e3 in smt::theory_lra::imp::var_value_eq::operator()(int, int) const /root/z3/build/../src/smt/theory_lra.cpp:190:25
......
SUMMARY: AddressSanitizer: heap-use-after-free /root/z3/build/../src/math/polynomial/algebraic_numbers.h:371:40 in algebraic_numbers::anum::is_basic() const
merlinsun commented 11 months ago

A possible related case:

$ cat delta.smt2
(declare-const x Bool)
(declare-fun r () Real)
(declare-fun v () Real)
(declare-fun va () Real)
(assert (exists ((a Real)) (or (< 0.0 (/ va a)) (and x (< (* r v v) r)))))
(check-sat)
NikolajBjorner commented 11 months ago

this doesn't repro on my side. Do you have any idea of where to point to blame? Lacking a repro, a more complete stack may help as well.

merlinsun commented 11 months ago

Sorry to hear that you're unable to reproduce the bug, @NikolajBjorner. I built z3 in debug mode with ASAN and CC=clang CXX=clang++, and the complete stack is:

=================================================================
==19911==ERROR: AddressSanitizer: heap-use-after-free on address 0x60b0000122a0 at pc 0x0000048cff61 bp 0x7fff22d4d640 sp 0x7fff22d4d638
READ of size 8 at 0x60b0000122a0 thread T0
    #0 0x48cff60 in algebraic_numbers::anum::is_basic() const /root/z3/build/../src/math/polynomial/algebraic_numbers.h:371:40
    #1 0x48c72e0 in algebraic_numbers::manager::imp::compare(algebraic_numbers::anum&, algebraic_numbers::anum&) /root/z3/build/../src/math/polynomial/algebraic_numbers.cpp:1950:19
    #2 0x48c7414 in algebraic_numbers::manager::imp::eq(algebraic_numbers::anum&, algebraic_numbers::anum&) /root/z3/build/../src/math/polynomial/algebraic_numbers.cpp:1965:20
    #3 0x48b493c in algebraic_numbers::manager::eq(algebraic_numbers::anum const&, algebraic_numbers::anum const&) /root/z3/build/../src/math/polynomial/algebraic_numbers.cpp:3045:23
    #4 0x24c4233 in smt::theory_lra::imp::is_eq(int, int) /root/z3/build/../src/smt/theory_lra.cpp:1599:32
    #5 0x24c7d33 in smt::theory_lra::imp::var_value_eq::operator()(int, int) const /root/z3/build/../src/smt/theory_lra.cpp:189:25
    #6 0x24c76a6 in core_hashtable<int_hash_entry<-2147483648, -2147483647>, smt::theory_lra::imp::var_value_hash, smt::theory_lra::imp::var_value_eq>::equals(int const&, int const&) const /root/z3/build/../src/util/hashtable.h:153:74
    #7 0x24c6cbf in core_hashtable<int_hash_entry<-2147483648, -2147483647>, smt::theory_lra::imp::var_value_hash, smt::theory_lra::imp::var_value_eq>::insert_if_not_there_core(int&&, int_hash_entry<-2147483648, -2147483647>*&) /root/z3/build/../src/util/hashtable.h:455:13
    #8 0x24c68e6 in core_hashtable<int_hash_entry<-2147483648, -2147483647>, smt::theory_lra::imp::var_value_hash, smt::theory_lra::imp::var_value_eq>::insert_if_not_there_core(int const&, int_hash_entry<-2147483648, -2147483647>*&) /root/z3/build/../src/util/hashtable.h:466:16
    #9 0x24c3d28 in core_hashtable<int_hash_entry<-2147483648, -2147483647>, smt::theory_lra::imp::var_value_hash, smt::theory_lra::imp::var_value_eq>::insert_if_not_there(int const&) /root/z3/build/../src/util/hashtable.h:476:9
    #10 0x24a2f02 in smt::theory_lra::imp::assume_eqs() /root/z3/build/../src/smt/theory_lra.cpp:1554:44
    #11 0x245f63a in smt::theory_lra::imp::final_check_eh() /root/z3/build/../src/smt/theory_lra.cpp:1676:17
    #12 0x24575a2 in smt::theory_lra::final_check_eh() /root/z3/build/../src/smt/theory_lra.cpp:3977:19
    #13 0x1dcfdef in smt::context::final_check() /root/z3/build/../src/smt/smt_context.cpp:4021:26
    #14 0x1dcb6dd in smt::context::bounded_search() /root/z3/build/../src/smt/smt_context.cpp:3937:42
    #15 0x1dc6a52 in smt::context::search() /root/z3/build/../src/smt/smt_context.cpp:3768:22
    #16 0x1dc4745 in smt::context::setup_and_check(bool) /root/z3/build/../src/smt/smt_context.cpp:3580:35
    #17 0x200ac81 in smt::kernel::setup_and_check() /root/z3/build/../src/smt/smt_kernel.cpp:124:32
    #18 0x14622a5 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/smt/tactic/smt_tactic_core.cpp:207:32
    #19 0x32798bf in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:122:19
    #20 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #21 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #22 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #23 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #24 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #25 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #26 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #27 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #28 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #29 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #30 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #31 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #32 0x32798bf in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:122:19
    #33 0x328b84e in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:874:14
    #34 0x32bac3c in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactic.cpp:165:9
    #35 0x32bb4b4 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) /root/z3/build/../src/tactic/tactic.cpp:185:9
    #36 0x30de999 in (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) /root/z3/build/../src/solver/tactic2solver.cpp:241:17
    #37 0x30d9eba in solver_na2as::check_sat_core(unsigned int, expr* const*) /root/z3/build/../src/solver/solver_na2as.cpp:67:12
    #38 0x311a1eb in combined_solver::check_sat_core(unsigned int, expr* const*) /root/z3/build/../src/solver/combined_solver.cpp:253:27
    #39 0x3106c2a in solver::check_sat(unsigned int, expr* const*) /root/z3/build/../src/solver/solver.cpp:318:13
    #40 0x303166d in cmd_context::check_sat(unsigned int, expr* const*) /root/z3/build/../src/cmd_context/cmd_context.cpp:1776:27
    #41 0x2faa95a in smt2::parser::parse_check_sat() /root/z3/build/../src/parsers/smt2/smt2parser.cpp:2633:19
    #42 0x2fa78dc in smt2::parser::parse_cmd() /root/z3/build/../src/parsers/smt2/smt2parser.cpp:2973:17
    #43 0x2fa193f in smt2::parser::operator()() /root/z3/build/../src/parsers/smt2/smt2parser.cpp:3191:29
    #44 0x2f9fd8c in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) /root/z3/build/../src/parsers/smt2/smt2parser.cpp:3242:12
    #45 0x508c33 in read_smtlib2_commands(char const*) /root/z3/build/../src/shell/smtlib_frontend.cpp:182:18
    #46 0x5593a7 in main /root/z3/build/../src/shell/main.cpp:384:28
    #47 0x7f3b653a8082 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x24082)
    #48 0x44747d in _start (/root/z3/build/z3+0x44747d)

0x60b0000122a0 is located 64 bytes inside of 104-byte region [0x60b000012260,0x60b0000122c8)
freed by thread T0 here:
    #0 0x4bfed9 in realloc (/root/z3/build/z3+0x4bfed9)
    #1 0x4a47067 in memory::reallocate(void*, unsigned long) /root/z3/build/../src/util/memory_manager.cpp:334:15
    #2 0x5ddb0e in vector<algebraic_numbers::anum, false, unsigned int>::expand_vector() /root/z3/build/../src/util/vector.h:205:28
    #3 0x5dd3cd in vector<algebraic_numbers::anum, false, unsigned int>::push_back(algebraic_numbers::anum&&) /root/z3/build/../src/util/vector.h:542:13
    #4 0x5dd1c3 in _scoped_numeral_vector<algebraic_numbers::manager>::push_back(algebraic_numbers::anum const&) /root/z3/build/../src/util/scoped_numeral_vector.h:52:45
    #5 0x3d145b1 in nra::solver::imp::value(unsigned int) /root/z3/build/../src/math/lp/nra_solver.cpp:553:27
    #6 0x3d0ed02 in nra::solver::value(unsigned int) /root/z3/build/../src/math/lp/nra_solver.cpp:623:19
    #7 0x3b997ed in nla::solver::am_value(unsigned int) const /root/z3/build/../src/math/lp/nla_solver.cpp:88:30
    #8 0x24c61b9 in smt::theory_lra::imp::nl_value(int, _scoped_numeral<algebraic_numbers::manager>&) const /root/z3/build/../src/smt/theory_lra.cpp:3415:27
    #9 0x24c4223 in smt::theory_lra::imp::is_eq(int, int) /root/z3/build/../src/smt/theory_lra.cpp:1599:64
    #10 0x24c7d33 in smt::theory_lra::imp::var_value_eq::operator()(int, int) const /root/z3/build/../src/smt/theory_lra.cpp:189:25
    #11 0x24c76a6 in core_hashtable<int_hash_entry<-2147483648, -2147483647>, smt::theory_lra::imp::var_value_hash, smt::theory_lra::imp::var_value_eq>::equals(int const&, int const&) const /root/z3/build/../src/util/hashtable.h:153:74
    #12 0x24c6cbf in core_hashtable<int_hash_entry<-2147483648, -2147483647>, smt::theory_lra::imp::var_value_hash, smt::theory_lra::imp::var_value_eq>::insert_if_not_there_core(int&&, int_hash_entry<-2147483648, -2147483647>*&) /root/z3/build/../src/util/hashtable.h:455:13
    #13 0x24c68e6 in core_hashtable<int_hash_entry<-2147483648, -2147483647>, smt::theory_lra::imp::var_value_hash, smt::theory_lra::imp::var_value_eq>::insert_if_not_there_core(int const&, int_hash_entry<-2147483648, -2147483647>*&) /root/z3/build/../src/util/hashtable.h:466:16
    #14 0x24c3d28 in core_hashtable<int_hash_entry<-2147483648, -2147483647>, smt::theory_lra::imp::var_value_hash, smt::theory_lra::imp::var_value_eq>::insert_if_not_there(int const&) /root/z3/build/../src/util/hashtable.h:476:9
    #15 0x24a2f02 in smt::theory_lra::imp::assume_eqs() /root/z3/build/../src/smt/theory_lra.cpp:1554:44
    #16 0x245f63a in smt::theory_lra::imp::final_check_eh() /root/z3/build/../src/smt/theory_lra.cpp:1676:17
    #17 0x24575a2 in smt::theory_lra::final_check_eh() /root/z3/build/../src/smt/theory_lra.cpp:3977:19
    #18 0x1dcfdef in smt::context::final_check() /root/z3/build/../src/smt/smt_context.cpp:4021:26
    #19 0x1dcb6dd in smt::context::bounded_search() /root/z3/build/../src/smt/smt_context.cpp:3937:42
    #20 0x1dc6a52 in smt::context::search() /root/z3/build/../src/smt/smt_context.cpp:3768:22
    #21 0x1dc4745 in smt::context::setup_and_check(bool) /root/z3/build/../src/smt/smt_context.cpp:3580:35
    #22 0x200ac81 in smt::kernel::setup_and_check() /root/z3/build/../src/smt/smt_kernel.cpp:124:32
    #23 0x14622a5 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/smt/tactic/smt_tactic_core.cpp:207:32
    #24 0x32798bf in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:122:19
    #25 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #26 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #27 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #28 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #29 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19

previously allocated by thread T0 here:
    #0 0x4bfed9 in realloc (/root/z3/build/z3+0x4bfed9)
    #1 0x4a47067 in memory::reallocate(void*, unsigned long) /root/z3/build/../src/util/memory_manager.cpp:334:15
    #2 0x5ddb0e in vector<algebraic_numbers::anum, false, unsigned int>::expand_vector() /root/z3/build/../src/util/vector.h:205:28
    #3 0x5dd3cd in vector<algebraic_numbers::anum, false, unsigned int>::push_back(algebraic_numbers::anum&&) /root/z3/build/../src/util/vector.h:542:13
    #4 0x5dd1c3 in _scoped_numeral_vector<algebraic_numbers::manager>::push_back(algebraic_numbers::anum const&) /root/z3/build/../src/util/scoped_numeral_vector.h:52:45
    #5 0x3d145b1 in nra::solver::imp::value(unsigned int) /root/z3/build/../src/math/lp/nra_solver.cpp:553:27
    #6 0x3d1b71e in nra::solver::imp::check_monic(nla::mon_eq const&) /root/z3/build/../src/math/lp/nra_solver.cpp:286:24
    #7 0x3d1010e in nra::solver::imp::check() /root/z3/build/../src/math/lp/nra_solver.cpp:174:22
    #8 0x3d0eb6c in nra::solver::check() /root/z3/build/../src/math/lp/nra_solver.cpp:603:19
    #9 0x3c0d470 in nla::core::bounded_nlsat() /root/z3/build/../src/math/lp/nla_core.cpp:1635:21
    #10 0x3c0b1cf in nla::core::check() /root/z3/build/../src/math/lp/nla_core.cpp:1575:15
    #11 0x3b9937c in nla::solver::check() /root/z3/build/../src/math/lp/nla_solver.cpp:46:24
    #12 0x24c138d in smt::theory_lra::imp::check_nla_continue() /root/z3/build/../src/smt/theory_lra.cpp:2033:26
    #13 0x24a26d0 in smt::theory_lra::imp::check_nla() /root/z3/build/../src/smt/theory_lra.cpp:2055:16
    #14 0x245f3cb in smt::theory_lra::imp::final_check_eh() /root/z3/build/../src/smt/theory_lra.cpp:1665:21
    #15 0x24575a2 in smt::theory_lra::final_check_eh() /root/z3/build/../src/smt/theory_lra.cpp:3977:19
    #16 0x1dcfdef in smt::context::final_check() /root/z3/build/../src/smt/smt_context.cpp:4021:26
    #17 0x1dcb6dd in smt::context::bounded_search() /root/z3/build/../src/smt/smt_context.cpp:3937:42
    #18 0x1dc6a52 in smt::context::search() /root/z3/build/../src/smt/smt_context.cpp:3768:22
    #19 0x1dc4745 in smt::context::setup_and_check(bool) /root/z3/build/../src/smt/smt_context.cpp:3580:35
    #20 0x200ac81 in smt::kernel::setup_and_check() /root/z3/build/../src/smt/smt_kernel.cpp:124:32
    #21 0x14622a5 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/smt/tactic/smt_tactic_core.cpp:207:32
    #22 0x32798bf in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:122:19
    #23 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #24 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #25 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #26 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #27 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #28 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19
    #29 0x328ee43 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1153:19

SUMMARY: AddressSanitizer: heap-use-after-free /root/z3/build/../src/math/polynomial/algebraic_numbers.h:371:40 in algebraic_numbers::anum::is_basic() const
Shadow bytes around the buggy address:
  0x0c167fffa400: 00 fa fa fa fa fa fa fa fa fa fd fd fd fd fd fd
  0x0c167fffa410: fd fd fd fd fd fd fd fa fa fa fa fa fa fa fa fa
  0x0c167fffa420: 00 00 00 00 00 00 00 00 00 00 00 00 00 fa fa fa
  0x0c167fffa430: fa fa fa fa fa fa 00 00 00 00 00 00 00 00 00 00
  0x0c167fffa440: 00 00 00 fa fa fa fa fa fa fa fa fa fd fd fd fd
=>0x0c167fffa450: fd fd fd fd[fd]fd fd fd fd fa fa fa fa fa fa fa
  0x0c167fffa460: fa fa fd fd fd fd fd fd fd fd fd fd fd fd fd fa
  0x0c167fffa470: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c167fffa480: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c167fffa490: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c167fffa4a0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa 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
  Shadow gap:              cc
==19911==ABORTING
merlinsun commented 11 months ago

I've bisected the issue and narrowed it down to one of the following commits: https://github.com/Z3Prover/z3/commit/20c54048f79d9fb57650ca390c44be5a917e390a, https://github.com/Z3Prover/z3/commit/4434cee5df67251c3402ff881de48739e0f0756e, https://github.com/Z3Prover/z3/commit/702744f1397b46497e858fe2efbac89df7b1668f, or https://github.com/Z3Prover/z3/commit/76f9e1d2b34524a583d156dc52d251119fceb73d. However, due to build issues, I'm unable to determine which commit exactly introduces the issue.

If there's anything else I can provide to help you investigate the issue, please let me know.

NikolajBjorner commented 11 months ago

fixed