Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

(smt.threads=2) segfault/stack-overflow on QF_ADTLIA formula #5297

Closed
zhendongsu opened this issue May 23, 2021 · 0 comments
Closed

(smt.threads=2) segfault/stack-overflow on QF_ADTLIA formula #5297

zhendongsu opened this issue May 23, 2021 · 0 comments

Comments

@zhendongsu
Copy link

Commit: f1545b0
OS: Ubuntu 18.04

[523] % z3release smt.threads=2 small.smt2 
Segmentation fault
[524] % z3debug smt.threads=2 small.smt2 
Segmentation fault
[525] % z3san smt.threads=2 small.smt2 
ASAN:DEADLYSIGNAL
=================================================================
==15035==ERROR: AddressSanitizer: stack-overflow on address 0x7ffe7399dff0 (pc 0x564a89d3fc94 bp 0x7ffe7399e230 sp 0x7ffe7399dfc0 T0)
    #0 0x564a89d3fc93 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2153
    #1 0x564a89d2fe88 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2273
    #2 0x564a88a71d98 in ast_manager::mk_app(func_decl*, ref_vector<expr, ast_manager> const&) ../src/ast/ast.h:1824
    #3 0x564a88a71d98 in datatype_factory::get_fresh_value(sort*) ../src/model/datatype_factory.cpp:177
    #4 0x564a879e8f85 in proto_model::get_fresh_value(sort*) ../src/smt/proto_model/proto_model.cpp:324
    #5 0x564a889f2fc8 in array_factory::get_fresh_value(sort*) ../src/model/array_factory.cpp:135
    #6 0x564a879e8f85 in proto_model::get_fresh_value(sort*) ../src/smt/proto_model/proto_model.cpp:324
    #7 0x564a88a7197c in datatype_factory::get_fresh_value(sort*) ../src/model/datatype_factory.cpp:166
...
SUMMARY: AddressSanitizer: stack-overflow ../src/ast/ast.cpp:2153 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*)
==15035==ABORTING
[526] % 
[526] % cat small.smt2 
(declare-datatypes ((a 0)) (((f) (g (e (Array Int a))))))
(declare-fun b () a)
(declare-fun c () a)
(declare-fun d () a)
(assert (distinct b c d))
(check-sat)
[527] %
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant