From 5c6ee647a9d1dfa3b404aa87736a79aa612fa463 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 10 Aug 2013 22:05:04 -0700 Subject: [PATCH] Fix bug in has_free_vars_fn. Add optimization to type_checker. Signed-off-by: Leonardo de Moura --- src/kernel/free_vars.cpp | 2 +- src/kernel/type_check.cpp | 4 +++- src/tests/kernel/type_check.cpp | 2 +- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 8daa27b773..567a6e5ac4 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -63,7 +63,7 @@ protected: break; } - if (m_set_closed_flag && !result) + if (m_set_closed_flag && !result && offset == 0) e.raw()->set_closed(); return result; diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp index d566d2a629..2d62a25e2f 100644 --- a/src/kernel/type_check.cpp +++ b/src/kernel/type_check.cpp @@ -128,7 +128,9 @@ struct infer_type_fn { buffer << "\nin context:\n" << ctx; throw exception(buffer.str()); } - if (closed(c)) + if (closed(abst_body(f_t))) + f_t = abst_body(f_t); + else if (closed(c)) f_t = instantiate_with_closed(abst_body(f_t), c); else f_t = instantiate(abst_body(f_t), c); diff --git a/src/tests/kernel/type_check.cpp b/src/tests/kernel/type_check.cpp index 893d12824b..18534baa3d 100644 --- a/src/tests/kernel/type_check.cpp +++ b/src/tests/kernel/type_check.cpp @@ -89,7 +89,7 @@ static void tst5() { env.add_var("P", Bool); expr P = Const("P"); expr H = Const("H"); - unsigned n = 500; + unsigned n = 4000; expr prop = P; expr pr = H; for (unsigned i = 1; i < n; i++) {