stack-use-after-scope at algebraic_numbers.h:372

[rainoftime]

Hi, for the following formula

(set-logic NRA)
(declare-const r3 Real)
(declare-const r16 Real)
(assert (not (exists ((q7 Real) (q8 Bool) (q9 Real)) (< r3 r16))))
(check-sat-using (then add-bounds ctx-solver-simplify qfnia))

asan detects a stack-use-after-scope issue in z3 (commit 9be7bda)

==3717==ERROR: AddressSanitizer: stack-use-after-scope on address 0x7ffea86323c0 at pc 0x000002a79d23 bp 0x7ffea8632300 sp 0x7ffea86322f0
READ of size 8 at 0x7ffea86323c0 thread T0
    #0 0x2a79d22 in algebraic_numbers::anum::is_basic() const ../src/math/polynomial/algebraic_numbers.h:372
    #1 0x2a82d3b in algebraic_numbers::manager::imp::save_intervals::restore_if_too_small() ../src/math/polynomial/algebraic_numbers.cpp:965
    #2 0x2a7d0eb in algebraic_numbers::manager::imp::is_rational(algebraic_numbers::anum&) ../src/math/polynomial/algebraic_numbers.cpp:334
    #3 0x2a76742 in algebraic_numbers::manager::is_rational(algebraic_numbers::anum const&) ../src/math/polynomial/algebraic_numbers.cpp:2887
    #4 0x2874e87 in arith_decl_plugin::mk_numeral(algebraic_numbers::anum const&, bool) ../src/ast/arith_decl_plugin.cpp:79
    #5 0x55d19c in arith_util::mk_numeral(algebraic_numbers::anum const&, bool) ../src/ast/arith_decl_plugin.h:406
    #6 0x1f77f73 in arith_rewriter::mk_power_core(expr*, expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/arith_rewriter.cpp:1213
    #7 0x1f6636d in arith_rewriter::mk_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/arith_
rewriter.cpp:76
    #8 0x1e75a28 in mev::evaluator_cfg::reduce_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_m
anager>&) ../src/model/model_evaluator.cpp:217
    #9 0x1e74a2c in mev::evaluator_cfg::reduce_app(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manage
r>&) ../src/model/model_evaluator.cpp:148
    #10 0x1e88f8c in void rewriter_tpl<mev::evaluator_cfg>::process_app<false>(app*, rewriter_core::frame&) ../src/ast/rewriter/rewriter_def.h:
291
    #11 0x1e82bea in void rewriter_tpl<mev::evaluator_cfg>::resume_core<false>(obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/
ast/rewriter/rewriter_def.h:754
    #12 0x1e7fe2b in void rewriter_tpl<mev::evaluator_cfg>::main_loop<false>(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ..
/src/ast/rewriter/rewriter_def.h:713
    #13 0x1e7ee8c in rewriter_tpl<mev::evaluator_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/re
writer/rewriter_def.h:785
    #14 0x1e7e0c8 in rewriter_tpl<mev::evaluator_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/rewriter.h:355
    #15 0x1e71a57 in model_evaluator::operator()(expr*, obj_ref<expr, ast_manager>&) ../src/model/model_evaluator.cpp:670
    #16 0x1e2a3c2 in generic_model_converter::operator()(ref<model>&) ../src/tactic/generic_model_converter.cpp:57
    #17 0x1df72f3 in concat_model_converter::operator()(ref<model>&) ../src/tactic/model_converter.cpp:80
    #18 0x1df72f3 in concat_model_converter::operator()(ref<model>&) ../src/tactic/model_converter.cpp:80
    #19 0x1df6f9a in model_converter2model(ast_manager&, model_converter*, ref<model>&) ../src/tactic/model_converter.cpp:181
    #20 0x1e07028 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manage
r::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src
/tactic/tactic.cpp:189
    #21 0x1cfd76d in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
    #22 0x1cb6878 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
    #23 0x1cb7169 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
    #24 0x1cb85ef in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #25 0x1c92576 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:
3179
    #26 0x46f5a1 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #27 0x4598ac in main ../src/shell/main.cpp:352

[NikolajBjorner]

my guess is that this is a false positive because the code uses tagged pointers