Closed wintered closed 4 years ago
[560] % z3 small.smt2 ASSERTION VIOLATION File: ../src/ast/ast.cpp Line: 431 UNREACHABLE CODE WAS REACHED. (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB a [561] % z3release small.smt2 unknown [562] % z3san small.smt2 ASAN:DEADLYSIGNAL ================================================================= ==5458==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000018 (pc 0x559d6641a609 bp 0x7ffee8ef0d70 sp 0x7ffee8ef0d40 T0) ==5458==The signal is caused by a READ memory access. ==5458==Hint: address points to the zero page. #0 0x559d6641a608 in smt::enode::is_cgr() const ../src/smt/smt_enode.h:301 #1 0x559d6641a608 in smt::context::undo_mk_enode() ../src/smt/smt_internalizer.cpp:1005 #2 0x559d65d91b7f in void undo_trail_stack<smt::context>(smt::context&, ptr_vector<trail<smt::context> >&, unsigned int) ../src/util/trail.h:343 #3 0x559d65d753a7 in smt::context::undo_trail_stack(unsigned int) ../src/smt/smt_context.cpp:1918 #4 0x559d65d753a7 in smt::context::pop_scope_core(unsigned int) ../src/smt/smt_context.cpp:2377 #5 0x559d65d7701c in smt::context::resolve_conflict() ../src/smt/smt_context.cpp:4016 #6 0x559d65d89694 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3726 #7 0x559d65d8a237 in smt::context::search() ../src/smt/smt_context.cpp:3599 #8 0x559d65d8cf3d in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3422 #9 0x559d65c0e8cf in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201 #10 0x559d6769a493 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:304 #11 0x559d676a19f7 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #12 0x559d67694351 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #13 0x559d676a0a01 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111 #14 0x559d676a19f7 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #15 0x559d676033ea in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148 #16 0x559d676056ed 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 #17 0x559d673b57b0 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223 #18 0x559d67344eb8 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895 #19 0x559d6734bb2c in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001 #20 0x559d6734bb2c in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130 #21 0x559d673031c5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179 #22 0x559d64993eb6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89 #23 0x559d6496c7ae in main ../src/shell/main.cpp:352 #24 0x7f588d3d2b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96) #25 0x559d64980529 in _start (/home/suz/software/z3san/build-04242020011206-470e87a/z3+0x1f7529) AddressSanitizer can not provide additional info. SUMMARY: AddressSanitizer: SEGV ../src/smt/smt_enode.h:301 in smt::enode::is_cgr() const ==5458==ABORTING [563] % [563] % cat small.smt2 (set-option :smt.random_seed 2) (set-option :trace true) (set-option :smt.clause_proof true) (set-option :smt.dack.eq true) (declare-datatypes ((Lst 0) (Nat 0)) (((cons (head Nat) (tail Lst)) (nil)) ((succ (pred Nat)) (zero)))) (declare-fun len (Lst) Nat) (assert (= (len nil) zero)) (assert (forall ((x Nat) (y Lst)) (= (len (cons x y)) (succ (len y))))) (declare-fun append (Lst Lst) Lst) (assert (forall ((x Lst)) (= (append nil x) x))) (assert (forall ((x Nat) (y Lst) (z Lst)) (= (append (cons x y) z) (cons x (append y z))))) (declare-fun rotate (Nat Lst) Lst) (assert (forall ((n Nat)) (= (rotate (succ n) nil) nil))) (declare-fun plus (Nat Nat) Nat) (assert (forall ((n Nat)) (= (plus zero n) n))) (assert (forall ((n Nat) (m Nat)) (= (plus (succ n) m) (succ (plus n m))))) (assert (not (forall ((x Lst) (y Lst)) (= (len (append x y)) (len (append y x)))))) (check-sat-using (then solve-eqs qfidl horn))
OS: Ubuntu 18.04 Commit: 470e87a
duplicate of #3991
OS: Ubuntu 18.04 Commit: 470e87a