Closed muchang closed 4 years ago
Hi, For this case, Z3 throws out a segmentation fault:
[559] % z3-4.8.7 small.smt2 unsat [560] % z3 small.smt2 ASSERTION VIOLATION File: ../src/ast/ast.h Line: 491 m_ref_count > 0 (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB a [561] % z3release small.smt2 unknown [562] % z3release small.smt2 unknown [563] % z3release small.smt2 Segmentation fault [564] % z3san small.smt2 ASAN:DEADLYSIGNAL ================================================================= ==27894==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000018 (pc 0x55b6a1224159 bp 0x7ffc6abdcdc0 sp 0x7ffc6abdcd90 T0) ==27894==The signal is caused by a READ memory access. ==27894==Hint: address points to the zero page. #0 0x55b6a1224158 in smt::enode::is_cgr() const ../src/smt/smt_enode.h:301 #1 0x55b6a1224158 in smt::context::undo_mk_enode() ../src/smt/smt_internalizer.cpp:1005 #2 0x55b6a0b9bd9f in void undo_trail_stack<smt::context>(smt::context&, ptr_vector<trail<smt::context> >&, unsigned int) ../src/util/trail.h:343 #3 0x55b6a0b7f5d7 in smt::context::undo_trail_stack(unsigned int) ../src/smt/smt_context.cpp:1918 #4 0x55b6a0b7f5d7 in smt::context::pop_scope_core(unsigned int) ../src/smt/smt_context.cpp:2377 #5 0x55b6a0b8124c in smt::context::resolve_conflict() ../src/smt/smt_context.cpp:4017 #6 0x55b6a0b938b4 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3727 #7 0x55b6a0b94457 in smt::context::search() ../src/smt/smt_context.cpp:3600 #8 0x55b6a0b9715d in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3423 #9 0x55b6a0a1874f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201 #10 0x55b6a2497257 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #11 0x55b6a23f8c4a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148 #12 0x55b6a23faf4d 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 #13 0x55b6a21ab010 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223 #14 0x55b6a213a718 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895 #15 0x55b6a214138c in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001 #16 0x55b6a214138c in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130 #17 0x55b6a20f8a25 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179 #18 0x55b69f79e456 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89 #19 0x55b69f776dce in main ../src/shell/main.cpp:352 #20 0x7fd184ec5b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96) #21 0x55b69f78aac9 in _start (/home/suz/software/z3san/build-04192020125842-f76c642/z3+0x1f7ac9) AddressSanitizer can not provide additional info. SUMMARY: AddressSanitizer: SEGV ../src/smt/smt_enode.h:301 in smt::enode::is_cgr() const ==27894==ABORTING [565] % [565] % cat small.smt2 (set-option :smt.random_seed 3) (set-option :trace true) (set-option :smt.dack.eq true) (declare-datatypes ((Nat 0)) (((succ (pred Nat)) zero))) (declare-datatypes ((Lst 0)) (((cons (head Nat) (tail Lst)) nil))) (declare-datatypes ((Pair 0) (ZLst 0)) (((mkpair (first Nat) (second Nat))) ((zcons (zhead Pair) (ztail ZLst)) znil))) (declare-fun nat-to-int (Nat) Int) (declare-fun append (Lst Lst) Lst) (declare-fun len (Lst) Nat) (declare-fun drop (Nat Lst) Lst) (declare-fun take (Nat Lst) Lst) (declare-fun zip (Lst Lst) ZLst) (declare-fun zappend (ZLst ZLst) ZLst) (assert (forall ((x Nat)) (>= (nat-to-int x) 0))) (assert (= (nat-to-int zero) 0)) (assert (forall ((x Nat) (y Lst)) (= (len (cons x y)) (succ (len y))))) (assert (forall ((x Nat)) (distinct (drop x nil) nil))) (assert (forall ((x Lst)) (= (drop zero x) x))) (assert (forall ((x Nat) (y Nat) (z Lst)) (= (drop (succ x) (cons y z)) (drop x z)))) (assert (forall ((x Nat) (y Nat) (z Lst)) (= (take (succ x) (cons y z)) (cons y (take x z))))) (assert (forall ((x Lst)) (= (zip nil x) znil))) (assert (forall ((x Lst)) (= (zip x nil) znil))) (assert (forall ((x Nat) (y Lst) (z Nat) (w Lst)) (= (zip (cons x y) (cons z w)) (zcons (mkpair x z) (zip y w))))) (assert (exists ((x ZLst)) (= (zappend znil x) x))) (assert (forall ((x Pair) (y ZLst) (z ZLst)) (= (zappend (zcons x y) z) (zcons x (zappend y z))))) (assert (not (forall ((xs Lst) (ys Lst) (zs Lst)) (= (zip (append xs ys) zs) (zappend (zip xs (take (len xs) zs)) (zip ys (drop (len xs) zs))))))) (check-sat-using auflira) [566] %
OS: Ubuntu 18.04 Commit: e1fa04b
pls file as duplicate of #3991
Hi, For this case, Z3 throws out a segmentation fault:
OS: Ubuntu 18.04 Commit: e1fa04b