Assertion violation at src/ast/ast.cpp:2910

[wintered]

[506] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 2910
to_app(get_fact(p1))->get_arg(1) == to_app(get_fact(p2))->get_arg(0)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[507] % z3release small.smt2
Segmentation fault
[508] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==11031==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000020 (pc 0x55957a981a71 bp 0x7ffc12f08830 sp 0x7ffc12f08810 T0)
==11031==The signal is caused by a READ memory access.
==11031==Hint: address points to the zero page.
  #0 0x55957a981a70 in ast::get_kind() const ../src/ast/ast.h:504
  #1 0x55957a981a70 in get_sort(expr const*) ../src/ast/ast.cpp:423
  #2 0x55957a981a70 in ast_manager::get_sort(expr const*) const ../src/ast/ast.h:1738
  #3 0x55957a981a70 in basic_decl_plugin::join(unsigned int, expr* const*) ../src/ast/ast.cpp:1100
  #4 0x55957a9c4cf0 in basic_decl_plugin::mk_func_decl(int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:1181
  #5 0x55957a98bf02 in ast_manager::mk_func_decl(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:2018
  #6 0x55957a9a65f6 in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:2024
  #7 0x55957a9afc0b in ast_manager::mk_app(int, int, expr*, expr*) ../src/ast/ast.cpp:2040
  #8 0x55957a9afc0b in ast_manager::mk_iff(expr*, expr*) ../src/ast/ast.h:2190
  #9 0x55957a9afc0b in ast_manager::mk_iff_false(app*) ../src/ast/ast.cpp:2869
  #10 0x5595785354ea in asserted_formulas::update_substitution(expr*, app*) ../src/smt/asserted_formulas.cpp:577
  #11 0x55957853a1b3 in asserted_formulas::commit(unsigned int) ../src/smt/asserted_formulas.cpp:498
  #12 0x55957853a1b3 in asserted_formulas::commit() ../src/smt/asserted_formulas.cpp:490
  #13 0x559577fe9d7b in smt::context::internalize_assertions() ../src/smt/smt_context.cpp:3084
  #14 0x55957802a197 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3477
  #15 0x5595797a9407 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #16 0x559579766a23 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:213
  #17 0x559579747f01 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #18 0x5595796a2fc0 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1551
  #19 0x5595795e9ca3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
  #20 0x5595795e9ca3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
  #21 0x5595795e9ca3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #22 0x5595795a11c5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #23 0x559576c31eb6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #24 0x559576c0a7ae in main ../src/shell/main.cpp:352
  #25 0x7f8f71fddb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #26 0x559576c1e529 in _start (/home/suz/software/z3san/build-04232020225820-7597396/z3+0x1f7529)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:504 in ast::get_kind() const
==11031==ABORTING
[509] % 
[509] % cat small.smt2
(set-option :proof true)
(declare-fun a () Bool)
(assert (not (! a :lblpos +)))
(check-sat a)
[510] %

OS: Ubuntu 18.04
Commit: 470e87a