michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(kernel/expr): check if the serializer works for applications with many argumets

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-15 17:09:46 -08:00
parent c096eec1d6
commit 5058e403b5
1 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/tests/kernel/expr.cpp
View file

@ -386,6 +386,22 @@ static void tst19() {
lean_assert(extend(extend(context(), "a", T2), "b", T2) != context({{"a", T1}, {"b", T2}}));
}
static void tst20() {
expr f = Const("f");
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
buffer<expr> args;
args.push_back(f);
for (unsigned i = 0; i < 200; i++) {
args.push_back(a);
args.push_back(b);
}
args.push_back(c);
expr t = mk_app(args);
check_serializer(t);
}
int main() {
save_stack_info();
lean_assert(sizeof(expr) == sizeof(optional<expr>));
@ -408,6 +424,7 @@ int main() {
tst17();
tst18();
tst19();
tst20();
std::cout << "sizeof(expr): " << sizeof(expr) << "\n";
std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n";
std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n";