(ufbv) Z3 Bus error (release) or segmentation fault (debug)

[muchang]

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

[552] % z3 small.smt2
Segmentation fault
[553] % z3release small.smt2
Bus error
[554] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==31497==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x559d85378ab5 bp 0x7fff44523120 sp 0x7fff44522d70 T0)
==31497==The signal is caused by a READ memory access.
==31497==Hint: address points to the zero page.
  #0 0x559d85378ab4 in cache_all_results ../src/ast/rewriter/rewriter.h:248
  #1 0x559d85378ab4 in must_cache ../src/ast/rewriter/rewriter.h:279
  #2 0x559d85378ab4 in visit<false> ../src/ast/rewriter/rewriter_def.h:159
  #3 0x559d8537f5ba in process_app<false> ../src/ast/rewriter/rewriter_def.h:260
  #4 0x559d8537f5ba in resume_core<false> ../src/ast/rewriter/rewriter_def.h:769
  #5 0x559d8539057a in main_loop<false> ../src/ast/rewriter/rewriter_def.h:728
  #6 0x559d8539057a in operator() ../src/ast/rewriter/rewriter_def.h:800
  #7 0x559d8539057a in th_rewriter::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/th_rewriter.cpp:860
  #8 0x559d84cebe80 in simplify_tactic::imp::operator()(goal&) ../src/tactic/core/simplify_tactic.cpp:57
  #9 0x559d84cebe80 in simplify_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/core/simplify_tactic.cpp:94
  #10 0x559d8512ed98 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:918
  #11 0x559d8513dba7 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #12 0x559d8513cbb1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
  #13 0x559d8513dba7 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #14 0x559d8513dba7 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #15 0x559d8513cbb1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
  #16 0x559d8513dba7 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #17 0x559d8513dba7 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #18 0x559d8513af02 in repeat_tactical::operator()(unsigned int, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:814
  #19 0x559d8513cbb1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
  #20 0x559d8509f59a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
  #21 0x559d850a189d 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
  #22 0x559d84e51910 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
  #23 0x559d84de0f38 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
  #24 0x559d84de7bac in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
  #25 0x559d84de7bac in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #26 0x559d84d9f245 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #27 0x559d824310b6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #28 0x559d8240994e in main ../src/shell/main.cpp:352
  #29 0x7fd10912cb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #30 0x559d8241d729 in _start (/home/suz/software/z3san/build-04262020232942-a0de244/z3+0x1f7729)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/rewriter/rewriter.h:248 in cache_all_results
==31497==ABORTING
[555] % 
[555] % cat small.smt2
(declare-sort c_unique)
(declare-sort c_ssorted)
(declare-sort e)
(declare-fun c_sort (e c_unique) c_ssorted)
(declare-fun f (Int) c_unique)
(declare-fun g (c_ssorted) Int)
(declare-fun h () e)
(declare-fun type_pointer (e) e)
(declare-fun type_alloc_table () e)
(declare-fun block_length (c_ssorted c_ssorted) Int)
(declare-fun j (c_ssorted) Int)
(declare-fun shift (c_ssorted Int) c_unique)
(declare-fun n (c_ssorted c_ssorted) Bool)
(declare-fun type_memory (e e) e)
(declare-fun acc (c_ssorted c_ssorted) c_unique)
(declare-fun ac (c_ssorted c_ssorted c_ssorted) c_unique)
(declare-fun type_pset (e) e)
(declare-fun ad (c_ssorted) c_unique)
(declare-fun bj (c_ssorted Int) c_unique)
(declare-fun s (c_ssorted c_ssorted Int) c_unique)
(declare-fun v (c_ssorted c_ssorted) c_unique)
(declare-fun not_in_pset (c_ssorted c_ssorted) Bool)
(declare-fun t (c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
(declare-fun bn (c_ssorted) Bool)
(declare-fun type_global () e)
(assert (forall ((?i c_unique)) (= (f (g (c_sort h ?i))) ?i)))
(assert (forall ((?k e) (?l c_unique) (?m c_unique)) (let ((?r (c_sort
 type_alloc_table ?l)) (?o (c_sort (type_pointer ?k) ?m)) (?aa 0)) (=
 (n ?r ?o) (< ?aa (block_length ?r ?o ))))))
(assert (exists ((?ab e)) (forall ((?p c_unique) (?q c_unique)) (let
 ((?o (type_pointer ?ab))) (let ((?r (c_sort ?o ?q))) (and (= 0 (j
 ?r)) (= ?p ?q)))))))
(assert (forall ((?u e) (?y e) (?w c_unique) (?ae c_unique) (?af
 c_unique)) (let ((?o (type_pointer ?u))) (= (forall ((?ag c_unique))
 (let ((?aa (c_sort (type_pointer ?y) ?ag))) (=(= ?af (acc (c_sort
 (type_memory ?o ?y) ?ae) ?aa)) (not_in_pset ?aa (c_sort (type_pset
 ?y) ?w))))) (not_in_pset (c_sort (type_pset ?y) ?w) (c_sort
 (type_memory ?o ?y) ?ae ))))))
(assert (forall ((?ah e) (?ai c_unique) (?aj c_unique) (?ak Int)) (let
 ((?o (type_pset ?ah))) (= (forall ((?al c_unique)) (or (forall ((?am
 Int)) (=(<= ?ak) (not (= ?ai (shift (c_sort (type_pointer ?ah) ?al)
 ?am))))))) (not_in_pset (c_sort (type_pointer ?ah) ?ai) (c_sort ?o
 (bj (c_sort ?o ?aj) ?ak)))))))
(assert (forall ((?an e) (?x e) (?ao c_unique) (?ap c_unique) (?aq
 c_unique) (?ar Int)) (let ((?o (type_pointer ?x))) (= (forall ((?bk
 c_unique)) (=(not (not_in_pset (c_sort (type_pointer ?an) ?bk)
 (c_sort (type_pset ?an) ?ap))) (forall ((?z Int)) (let ((?aa
 (type_pointer ?an))) (=(= ?ar ?z) (not (= ?ao (acc (c_sort
 (type_memory ?o ?an) ?aq) (c_sort ?aa (shift (c_sort ?aa ?bk)
 ?z)))))))))) (not_in_pset (c_sort ?o ?ao) (c_sort (type_pset ?x) (s
 (c_sort (type_pset ?an) ?ap) (c_sort (type_memory ?o ?an) ?aq)
 ?ar)))))))
(assert (forall ((?as e) (?bl e) (?at c_unique)) (= (bn (c_sort
 (type_memory (type_pointer ?bl) ?as) ?at)) (forall ((?bm c_unique)
 (?bo c_unique)) (let ((?aa (type_pointer ?bl)) (?o (c_sort
 type_alloc_table ?bo)) (?r (c_sort (type_pointer ?as) ?bm))) (n ?o
 (c_sort ?aa (acc (c_sort (type_memory ?aa ?as) ?at) ?r))))))))
(assert (not (forall ((?a c_unique) (?b c_unique) (?c c_unique) (?d
 c_unique) (?alloc c_unique) (?au c_unique)) (let ((?o (c_sort
 type_alloc_table ?alloc)) (?aa (type_pointer type_global))) (=> and
 (n ?o (c_sort ?aa ?c)) (forall ((?intM_global0 c_unique)) (let ((?av
 (c_sort ?aa ?a)) (?aw (c_sort ?aa ?b)) (?ax (type_memory h
 type_global))) (let ((?r (c_sort ?ax ?intM_global0)) (?ay (c_sort
 ?ax ?au)) (?az type_global )) (=> (t ?o ?ay ?r (c_sort ?az (v
 (c_sort ?az (ad ?aw)) (c_sort ?az (ad ?av))))) (xor (n ?o (c_sort
 ?aa ?c)) (forall ((?ba c_unique)) (=(= ?ba (acc ?r (c_sort ?aa ?c)))
 (forall ((?bb c_unique)) (=(= ?bb (acc ?r (c_sort ?aa ?d))) (forall
 ((?bc c_unique)) (=(= ?bc (acc ?r (c_sort ?aa ?c))) (forall ((?bd
 Int)) (=> (= (f ?bd) ?bc) (forall ((?be c_unique)) (=> (n ?o (c_sort
 ?aa ?c)) (forall ((?bf c_unique)) (=> (= ?bf (ac ?r (c_sort ?aa ?c)
 (c_sort h ?be))) (forall ((?bg c_unique)) (=> (= ?bg (ac (c_sort ?ax
 ?bf) (c_sort ?aa ?d) (c_sort h (f ?bd)))) (forall ((?bh c_unique))
 (let ((?bi (c_sort ?aa ?bh))) (= ?r ?bi)))))))))))))))))))))))))))
(check-sat-using ufbv)
[556] %

OS: Ubuntu 18.04
Commit: a0de244