fix(kernel/max_sharing): add example exposing bug in max_sharing_fn, and fix it
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
1c8e78e3ae
commit
508bccb0c5
2 changed files with 19 additions and 1 deletions
|
@ -45,7 +45,7 @@ struct max_sharing_fn::imp {
|
|||
res = update_mlocal(a, apply(mlocal_type(a)));
|
||||
break;
|
||||
}
|
||||
m_cache.insert(a);
|
||||
m_cache.insert(res);
|
||||
return res;
|
||||
}
|
||||
|
||||
|
|
|
@ -45,9 +45,27 @@ static void tst2() {
|
|||
lean_assert(is_eqp(arg1, arg2));
|
||||
}
|
||||
|
||||
static void tst3() {
|
||||
max_sharing_fn max_fn;
|
||||
expr a1 = Const("a");
|
||||
expr a2 = Const("a");
|
||||
expr a3 = Const("a");
|
||||
expr g = Const("g");
|
||||
expr f = Const("f");
|
||||
expr new_a1 = max_fn(a1);
|
||||
lean_assert(is_eqp(new_a1, a1));
|
||||
expr t1 = max_fn(f(a2));
|
||||
lean_assert(is_eqp(app_arg(t1), a1));
|
||||
expr t2 = max_fn(f(a2));
|
||||
lean_assert(is_eqp(t1, t2));
|
||||
expr t3 = max_fn(f(a3));
|
||||
lean_assert(is_eqp(t1, t3));
|
||||
}
|
||||
|
||||
int main() {
|
||||
save_stack_info();
|
||||
tst1();
|
||||
tst2();
|
||||
tst3();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue