(nnf) Segementation fault (release) or Assertion violation at ../src/util/parray.h Line: 336 (debug)

[muchang]

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

[507] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/util/parray.h
Line: 336
i < size(r)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[508] % z3release small.smt2
Segmentation fault
[509] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==10264==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000008 (pc 0x55d19a642a49 bp 0x7ffde5085670 sp 0x7ffde5085430 T0)
==10264==The signal is caused by a READ memory access.
==10264==Hint: address points to the zero page.
  #0 0x55d19a642a48 in nnf::imp::visit(expr*, bool, bool) ../src/ast/normal_forms/nnf.cpp:418
  #1 0x55d19a64af84 in nnf::imp::process(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/normal_forms/nnf.cpp:856
  #2 0x55d19a63cc0d in nnf::imp::operator()(expr*, ref_vector<expr, ast_manager>&, ref_vector<app, ast_manager>&, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/normal_forms/nnf.cpp:898
  #3 0x55d19a63cc0d in nnf::operator()(expr*, ref_vector<expr, ast_manager>&, ref_vector<app, ast_manager>&, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/normal_forms/nnf.cpp:928
  #4 0x55d199f0fc6e in nnf_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/core/nnf_tactic.cpp:75
  #5 0x55d19a49667a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
  #6 0x55d19a49897d 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
  #7 0x55d19a248a40 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
  #8 0x55d19a1d8148 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
  #9 0x55d19a1dedbc in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
  #10 0x55d19a1dedbc in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #11 0x55d19a196455 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179  
  #12 0x55d197834f66 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #13 0x55d19780d99e in main ../src/shell/main.cpp:352
  #14 0x7f79213edb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #15 0x55d1978215d9 in _start (/home/suz/software/z3san/build-04182020194526-bcbe802/z3+0x1f75d9)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/normal_forms/nnf.cpp:418 in nnf::imp::visit(expr*, bool, bool)
==10264==ABORTING
[510] %
[510] % cat small.smt2
(assert (exists ((a Int)) false))
(assert (forall ((b Int)) false))
(check-sat-using nnf)
[511] %

OS: Ubuntu 18.04 Commit: bcbe802

[NikolajBjorner]

yes, related to #4021