Segfault, stack-overflow ../src/ast/ast.cpp:2205

[zhendongsu]

Commit: dd27f7e
OS: Ubuntu 18.04

It appears to be a regression from 4.8.11.

[512] % z3release small.smt2 
Segmentation fault
[513] % z3debug small.smt2 
Segmentation fault
[514] % z3san small.smt2 
ASAN:DEADLYSIGNAL
=================================================================
==7340==ERROR: AddressSanitizer: stack-overflow on address 0x7fffc99badd8 (pc 0x55fe33c7e721 bp 0x7fffc99bb0e0 sp 0x7fffc99badb0 T0)
    #0 0x55fe33c7e720 in ast_manager::check_args(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2205
    #1 0x55fe33caa0b4 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2169
    #2 0x55fe33c99d08 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2271
    #3 0x55fe329b2968 in ast_manager::mk_app(func_decl*, ref_vector<expr, ast_manager> const&) ../src/ast/ast.h:1828
    #4 0x55fe329b2968 in datatype_factory::get_fresh_value(sort*) ../src/model/datatype_factory.cpp:184
    #5 0x55fe318b0905 in proto_model::get_fresh_value(sort*) ../src/smt/proto_model/proto_model.cpp:325
    #6 0x55fe329b2704 in datatype_factory::get_fresh_value(sort*) ../src/model/datatype_factory.cpp:173
    #7 0x55fe329b49c7 in datatype_factory::get_fresh_value(sort*) ../src/model/datatype_factory.cpp:225
    #8 0x55fe329b49c7 in datatype_factory::get_fresh_value(sort*) ../src/model/datatype_factory.cpp:225
    #9 0x55fe329b49c7 in datatype_factory::get_fresh_value(sort*) ../src/model/datatype_factory.cpp:225
...
SUMMARY: AddressSanitizer: stack-overflow ../src/ast/ast.cpp:2205 in ast_manager::check_args(func_decl*, unsigned int, expr* const*)
==7340==ABORTING
[515] % 
[515] % cat small.smt2 
(declare-fun p () Bool)
(declare-sort C 0)
(declare-sort h 0)
(declare-sort r 0)
(declare-datatypes ((i 0) (Ch 0) (a 0)) ((i) ((h (c i))) ((n) (ns (d Ch) (t a)))))
(declare-fun s () r)
(declare-fun e (a) C)
(declare-fun u (h a) Bool)
(declare-fun u (C C) Bool)
(declare-fun u (h C) C)
(declare-fun u (r C) h)
(assert (forall ((q C) (v2 h)) (= (and (forall ((v a)) p) (forall ((v a)) (not (u v2 v)))) (forall ((v a)) (or (not (u v2 v)) (u (e n) (u (u s q) q)))))))
(check-sat)