Segfault release built smt.arith.solver 4, smt.phase_selection 5, rewriter.eq2ineq true

[wintered]

[1005] % z3-4.8.7 small.smt2
unsat
[1006] % z3release small.smt2
WARNING: found non utvpi logic expression:
(>= (+ c d (* (- 1) (div b a))) 0)
Segmentation fault
[1007] % 
[1007] % cat small.smt2
(set-option :smt.arith.solver 4)
(set-option :smt.phase_selection 5)
(set-option :rewriter.eq2ineq true)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(assert (= 0 c 1))
(assert (or (= d 0) (= d 1)))
(assert (= (div b a) (+ d c) 1))
(check-sat)
[1008] %

OS: Ubuntu 18.04
Commit: fdabaa6

[NikolajBjorner]

this reproduces neither on Windows, nor on Ubuntu for me
Could you list the stack you get? Without a stack or repro I will have to close this as a fluke

[zhendongsu]

Nikolaj, here is what I see on the latest commit (db9d6d1):

[577] % z3san bug3903.smt2 
WARNING: found non utvpi logic expression:
(>= (+ c d (* (- 1) (div b a))) 0)

ASAN:DEADLYSIGNAL
=================================================================
==3967==ERROR: AddressSanitizer: SEGV on unknown address 0x62140001190c (pc 0x55e8e82a1b0e bp 0x7ffdfa5a5d20 sp 0x7ffdfa5a5a10 T0)
==3967==The signal is caused by a WRITE memory access.
    #0 0x55e8e82a1b0d in heap<dl_var_lt<smt::theory_utvpi<smt::rdl_ext>::GExt> >::move_up(int) ../src/util/heap.h:87
    #1 0x55e8e82a1b0d in heap<dl_var_lt<smt::theory_utvpi<smt::rdl_ext>::GExt> >::decreased(int) ../src/util/heap.h:222
    #2 0x55e8e82a1b0d in dl_graph<smt::theory_utvpi<smt::rdl_ext>::GExt>::make_feasible(int) ../src/smt/diff_logic.h:410
    #3 0x55e8e82a55bb in dl_graph<smt::theory_utvpi<smt::rdl_ext>::GExt>::enable_edge(int) ../src/smt/diff_logic.h:522
    #4 0x55e8e82a572a in smt::theory_utvpi<smt::rdl_ext>::enable_edge(int) ../src/smt/theory_utvpi_def.h:694
    #5 0x55e8e82a588e in smt::theory_utvpi<smt::rdl_ext>::propagate_atom(smt::theory_utvpi<smt::rdl_ext>::atom const&) ../src/smt/theory_utvpi_def.h:522
    #6 0x55e8e82a5a3f in smt::theory_utvpi<smt::rdl_ext>::propagate() ../src/smt/theory_utvpi_def.h:510
    #7 0x55e8e7a8f1b7 in smt::context::propagate_theories() ../src/smt/smt_context.cpp:1599
    #8 0x55e8e7a8f1b7 in smt::context::propagate() ../src/smt/smt_context.cpp:1682
    #9 0x55e8e7a9ab77 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3717
    #10 0x55e8e7a9b7d7 in smt::context::search() ../src/smt/smt_context.cpp:3601
    #11 0x55e8e7a9e4dd in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3424
    #12 0x55e8e791f8af in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201
    #13 0x55e8e937e597 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #14 0x55e8e9370da7 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:939
    #15 0x55e8e9377397 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:296
    #16 0x55e8e937e597 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #17 0x55e8e937e597 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #18 0x55e8e93713f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1031
    #19 0x55e8e93713f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1031
    #20 0x55e8e93713f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1031
    #21 0x55e8e93713f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1031
    #22 0x55e8e93713f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1031
    #23 0x55e8e93713f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1031
    #24 0x55e8e93713f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1031
    #25 0x55e8e93713f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1031
    #26 0x55e8e937e597 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #27 0x55e8e92dfdba in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
    #28 0x55e8e92e20bd 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> >&) ../src/tactic/tactic.cpp:168
    #29 0x55e8e91e0a18 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
    #30 0x55e8e91e7dd7 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #31 0x55e8e91a57e4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
    #32 0x55e8e91868d1 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #33 0x55e8e90d4c00 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1575
    #34 0x55e8e90272f3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #35 0x55e8e90272f3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #36 0x55e8e90272f3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #37 0x55e8e8fde815 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #38 0x55e8e66a7006 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #39 0x55e8e667fb0e in main ../src/shell/main.cpp:352
    #40 0x7f99c6f72b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #41 0x55e8e6693679 in _start (/home/suz/software/z3san/build-04112020152718-db9d6d1/z3+0x1f6679)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/util/heap.h:87 in heap<dl_var_lt<smt::theory_utvpi<smt::rdl_ext>::GExt> >::move_up(int)
==3967==ABORTING
[578] % 

@NikolajBjorner

[agurfinkel]

does not repro on osx either. Are you passing any additional options to ASAN that are not on by default?

[zhendongsu]

I built on Ubuntu 18.04 and used the following configuration command:

CFLAGS="-g -fsanitize=address -fno-omit-frame-pointer" CXXFLAGS="-g -fsanitize=address -fno-omit-frame-pointer" LDFLAGS="-fsanitize=address" python scripts/mk_make.py

[agurfinkel]

I do the same. There are also runtime flags that can be used to control asan behavior during execution. I thought you might be using these. I guess not.

[zhendongsu]

@NikolajBjorner
Nikolaj, this segfault still triggers on the latest commit (164a73f) on Ubuntu 18.04.