(qflia trace smt.phase_selection) Segmentation fault (release) or Assertion violation (debug) at ../src/smt/smt_enode.h Line: 284

[muchang]

Hi,
For this case, Z3 throws out a segmentation fault:

[708] % z3 small.smt2
(smt.diff_logic: non-diff logic expression (+ 1 (str.len s)))
unsat
sat
[709] % 
[709] % cat small.smt2
(set-option :smt.arith.solver 1)
(declare-fun s () String)
(assert (str.in.re (str.++ "a" s) (re.* (str.to.re "b"))))
(check-sat)
(check-sat-using unit-subsume-simplify)
[710] %

1 reply
Today at 3:07 PMView thread

Zhendong  3:03 PM
not the most sure about this one, but the behavior doesn't seem expected
3:04
could be related to https://github.com/Z3Prover/z3/issues/3935 (edited) 

Zhendong  4:48 PM
[608] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_enode.h
Line: 284
!m_mark2
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[609] % 
[609] % z3release small.smt2
Segmentation fault
[610] % 
[610] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==11519==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000008 (pc 0x55dce4831de2 bp 0x7ffd05a0ec60 sp 0x7ffd05a0eaa0 T0)
==11519==The signal is caused by a READ memory access.
==11519==Hint: address points to the zero page.
  #0 0x55dce4831de1 in smt::theory_datatype::occurs_check_explain(smt::enode*, smt::enode*) ../src/smt/theory_datatype.cpp:548
  #1 0x55dce483388f in smt::theory_datatype::occurs_check_enter(smt::enode*) ../src/smt/theory_datatype.cpp:602
  #2 0x55dce48348c7 in smt::theory_datatype::occurs_check(smt::enode*) ../src/smt/theory_datatype.cpp:653
  #3 0x55dce48360f7 in smt::theory_datatype::final_check_eh() ../src/smt/theory_datatype.cpp:478
  #4 0x55dce3c86984 in smt::context::final_check() ../src/smt/smt_context.cpp:3858
  #5 0x55dce3c96df6 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3774
  #6 0x55dce3c976f7 in smt::context::search() ../src/smt/smt_context.cpp:3601
  #7 0x55dce3c9a3fd in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3424
  #8 0x55dce3b1b7cf in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201
  #9 0x55dce55717ab in annotate_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1002
  #10 0x55dce556cc67 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:939
  #11 0x55dce5573257 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:296
  #12 0x55dce55793a1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
  #13 0x55dce557a457 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #14 0x55dce55717ab in annotate_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1002
  #15 0x55dce5573257 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:296
  #16 0x55dce557a457 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #17 0x55dce54dbc7a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
  #18 0x55dce54ddf7d 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
  #19 0x55dce528df70 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
  #20 0x55dce521d228 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
  #21 0x55dce5223e9c in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
  #22 0x55dce5223e9c in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #23 0x55dce51db535 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #24 0x55dce28a1f76 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #25 0x55dce287aa7e in main ../src/shell/main.cpp:352
  #26 0x7eff63722b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #27 0x55dce288e5e9 in _start (/home/suz/software/z3san/build-04122020180154-01c12c9/z3+0x1f65e9)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/smt/theory_datatype.cpp:548 in smt::theory_datatype::occurs_check_explain(smt::enode*, smt::enode*)
==11519==ABORTING
[611] % 
[611] % cat small.smt2
(set-option :smt.phase_selection 5)
(set-option :trace true)
(declare-datatypes ((a 0) (ba8 0)) (((ca4 (da5 ba8) (f a)) (ja7)) (k)))
(declare-fun e () a)
(declare-fun f (a a) a)
(declare-fun l (Int) a)
(declare-fun g (Int) a)
(assert
 (forall ((h Int))
 (and (distinct (f (l h) (g h))
    (ite ((_ is ja7) (l h)) (g h)
     (ite ((_ is k) (l h)) (ca4 (da5 (l h)) (f (l h) (g h))) e)))
  ((_ is ja7) (l h))
  (ite ((_ is ca4) (l h))
  (exists ((i Int)) (= (l i) (l h))) true))))
(check-sat-using qflia)
[612] %

AddressSanitizer may show the root cause.

OS: Ubuntu 18.04
Commit: 01c12c9