Incremental mode segmentation faults

[LeventErkok]

Fresh build of z3 seg-faults on Mac OSX for the following benchmark. This seems to happen quite often with Reals involved:

(set-option :produce-models true)
(set-logic ALL)
(define-fun s2 () Real (/ 4.0 1.0))
(declare-fun s0 () Real)
(define-fun s1 () Real (* s0 s0))
(define-fun s3 () Bool (= s1 s2))
(assert s3)
(check-sat)
(define-fun s4 () Real (/ 2.0 1.0))
(define-fun s5 () Bool (distinct s0 s4))
(assert s5)
(check-sat)

First check-sat goes through, but after the second check-sat, I get:

sat
[1]    79591 segmentation fault  z3 a.smt2

(Possibly the same root-cause as: https://github.com/Z3Prover/z3/issues/4324, but this one is rather new. #4324 also happens with z3 built about a week ago, while the above goes through with that version.)

[NikolajBjorner]

since Sunday, only on the Mac build. But we don't have a stack yet. If you can paste a stack it could help.

4324 is something else: it is connected to how string constraints are normalized. There is a separate bug open on this that is related.

[LeventErkok]

Sadly, if I do a debug build I do not get a segmentation fault. It runs producing two sat answers. Quite frustrating.

[aytey]

Just built 1dcbde4ec:

cassidy:build avj$ lldb z3
(lldb) target create "z3"
Current executable set to '/Users/avj/clones/z3/build/z3' (x86_64).
(lldb) run test.smt2
Process 62183 launched: '/Users/avj/clones/z3/build/z3' (x86_64)
sat
z3 was compiled with optimization - stepping may behave oddly; variables may not be available.
Process 62183 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=EXC_I386_GPFLT)
    frame #0: 0x0000000100af17bd z3`smt::theory_seq::theory_seq(smt::context&) [inlined] vector<automaton<sym_expr, sym_expr_manager>*, false, unsigned int>::vector(this=<unavailable>) at vector.h:138:9 [opt]
   135      typedef const T * const_iterator;
   136
   137      vector():
-> 138          m_data(nullptr) {
   139      }
   140
   141      vector(SZ s) {
Target 0: (z3) stopped.
(lldb) bt
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=EXC_I386_GPFLT)
  * frame #0: 0x0000000100af17bd z3`smt::theory_seq::theory_seq(smt::context&) [inlined] vector<automaton<sym_expr, sym_expr_manager>*, false, unsigned int>::vector(this=<unavailable>) at vector.h:138:9 [opt]
    frame #1: 0x0000000100af17ba z3`smt::theory_seq::theory_seq(smt::context&) [inlined] ptr_vector<automaton<sym_expr, sym_expr_manager> >::ptr_vector(this=<unavailable>) at vector.h:593 [opt]
    frame #2: 0x0000000100af17ba z3`smt::theory_seq::theory_seq(smt::context&) [inlined] ptr_vector<automaton<sym_expr, sym_expr_manager> >::ptr_vector(this=<unavailable>) at vector.h:593 [opt]
    frame #3: 0x0000000100af17ba z3`smt::theory_seq::theory_seq(smt::context&) [inlined] scoped_ptr_vector<automaton<sym_expr, sym_expr_manager> >::scoped_ptr_vector(this=<unavailable>) at scoped_ptr_vector.h:27 [opt]
    frame #4: 0x0000000100af17ba z3`smt::theory_seq::theory_seq(smt::context&) [inlined] scoped_ptr_vector<automaton<sym_expr, sym_expr_manager> >::scoped_ptr_vector(this=<unavailable>) at scoped_ptr_vector.h:27 [opt]
    frame #5: 0x0000000100af17ba z3`smt::theory_seq::theory_seq(this=0x0000000102929a08, ctx=<unavailable>) at theory_seq.cpp:277 [opt]
    frame #6: 0x0000000100919e37 z3`smt::setup::setup_seq_str(this=0x0000000103064890, st=<unavailable>) at smt_setup.cpp:0 [opt]
    frame #7: 0x0000000100915276 z3`smt::setup::setup_unknown(this=0x0000000103064890) at smt_setup.cpp:958:9 [opt]
    frame #8: 0x000000010091515b z3`smt::setup::operator(this=0x0000000103064890, cm=<unavailable>)(smt::config_mode) at smt_setup.cpp:65:25 [opt]
    frame #9: 0x00000001008c0f51 z3`smt::context::setup_context(this=0x0000000103064808, use_static_features=<unavailable>) at smt_context.cpp:3454:9 [opt]
    frame #10: 0x00000001008c0a07 z3`smt::context::check(this=0x0000000103064808, num_assumptions=0, assumptions=0x0000000000000000, reset_cancel=<unavailable>) at smt_context.cpp:3482:9 [opt]
    frame #11: 0x000000010067e82a z3`solver_na2as::check_sat_core(this=<unavailable>, num_assumptions=<unavailable>, assumptions=0x0000000101d88b10) at solver_na2as.cpp:67:12 [opt]
    frame #12: 0x00000001006744cf z3`combined_solver::check_sat_core(this=0x0000000101d884e8, num_assumptions=0, assumptions=0x0000000101d88b10) at combined_solver.cpp:219:38 [opt]
    frame #13: 0x000000010067d08d z3`solver::check_sat(this=0x0000000101d884e8, num_assumptions=0, assumptions=0x0000000101d88b10) at solver.cpp:330:13 [opt]
    frame #14: 0x000000010073d33e z3`cmd_context::check_sat(this=<unavailable>, num_assumptions=0, assumptions=0x0000000101d88b10) at cmd_context.cpp:1549:27 [opt]
    frame #15: 0x0000000100767434 z3`smt2::parser::parse_check_sat(this=0x00007ffeefbfe9f0) at smt2parser.cpp:2595:19 [opt]
    frame #16: 0x0000000100765b00 z3`smt2::parser::parse_cmd(this=<unavailable>) at smt2parser.cpp:379:17 [opt] [artificial]
    frame #17: 0x000000010076426b z3`smt2::parser::operator(this=0x00007ffeefbfe9f0)() at smt2parser.cpp:3129:29 [opt]
    frame #18: 0x000000010076419f z3`parse_smt2_commands(ctx=<unavailable>, is=<unavailable>, interactive=<unavailable>, ps=<unavailable>, filename=<unavailable>) at smt2parser.cpp:3178:12 [opt]
    frame #19: 0x0000000100fbd4f9 z3`read_smtlib2_commands(file_name="test.smt2") at smtlib_frontend.cpp:90:18 [opt]
    frame #20: 0x0000000100fbbd2d z3`main(argc=2, argv=<unavailable>) at main.cpp:352:28 [opt]
    frame #21: 0x00007fff6b981cc9 libdyld.dylib`start + 1
(lldb) q
Quitting LLDB will kill one or more processes. Do you really want to proceed: [Y/n] y

HTH

[NikolajBjorner]

OK, thanks, that is a good clue. @levnach also couldn't get the bug in debug mode.

[NikolajBjorner]

our Mac build is back in green after reshuffling the order on a few fields. I wonder if it is some alignment (bug in the compiler)?

[aytey]

This appears to be related to -O1 vs. -O2.

If I change cmake/cxx_compiler_flags_overrides.cmake to be -O1, things work fine. If I leave it as -O2, I get the segfault.

$ clang --version
Apple clang version 11.0.3 (clang-1103.0.32.29)
Target: x86_64-apple-darwin19.4.0
Thread model: posix
InstalledDir: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin

[aytey]

Interestingly, I just tried 1dcbde4ec on Ubuntu 20.04 with:

$ clang-11 --version
clang version 11.0.0-++20200513052626+1370757dd01-1~exp1~20200513153230.40
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/bin

and I do not get the segfault (admittedly 11.0.0 != 11.0.3).

[LeventErkok]

our Mac build is back in green after reshuffling the order on a few fields. I wonder if it is some alignment (bug in the compiler)?

I can confirm that this "shuffling" addresses the issue for me, thanks!

I'll leave the ticket open in case you want to investigate further.