From 69d9c8b95d3066064ec0186d5bacd90537ffa97b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Jul 2014 13:20:24 -0700 Subject: [PATCH] fix(tests): to reflect recent changes Signed-off-by: Leonardo de Moura --- src/tests/kernel/metavar.cpp | 7 ++----- tests/lua/subst1.lua | 4 ++-- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 7958a0f85..9d92b409e 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -91,14 +91,11 @@ static void tst2() { expr f = Const("f"); expr g = Const("g"); expr a = Const("a"); - lean_assert(s.occurs(m1, f(m1))); - lean_assert(!s.occurs(m2, f(m1))); s.assign(m1, f(m2), mk_assumption_justification(1)); - lean_assert(s.occurs(m2, f(m1))); s.assign(m2, g(a), mk_assumption_justification(2)); lean_assert(check_assumptions(s.get_assignment(m1)->second, {1})); - lean_assert(!s.occurs(m1, f(m1))); - lean_assert(!s.occurs(m2, f(m1))); + lean_assert(s.occurs(m1, f(m1))); + lean_assert(s.occurs(m2, f(m1))); lean_assert(!s.occurs(m1, f(m2))); lean_assert(!s.occurs(m1, f(a))); lean_assert(!s.occurs(m3, f(m1))); diff --git a/tests/lua/subst1.lua b/tests/lua/subst1.lua index f26ddadd2..b450ad372 100644 --- a/tests/lua/subst1.lua +++ b/tests/lua/subst1.lua @@ -24,8 +24,8 @@ assert(s:get_expr("m") == a) local m2 = mk_metavar("m2", Prop) s:assign(m2, f(m)) print(s:get_expr("m2")) -assert(not s:occurs(m, f(m2))) -assert(not s:occurs_expr("m", f(m2))) +assert(s:occurs(m, f(m2))) +assert(s:occurs_expr("m", f(m2))) print(s:get_level("u")) print(s:instantiate(mk_sort(u))) assert(s:instantiate(mk_sort(u)) == mk_sort(l))