From 7ea78551342ff1a1bfe36e2c7f9eaa44a2096a35 Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 5 Oct 2011 19:31:21 -0700 Subject: added membership tests --- Test/datatypes/t1.bpl | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'Test/datatypes') diff --git a/Test/datatypes/t1.bpl b/Test/datatypes/t1.bpl index 61409465..b56e26ae 100644 --- a/Test/datatypes/t1.bpl +++ b/Test/datatypes/t1.bpl @@ -16,5 +16,9 @@ procedure foo() assert value#node(node(x, nil())) == x; assert children#node(node(x, nil())) == nil(); - assert (cons(leaf(), nil()) == nil()); + assert (cons(leaf(), nil()) != nil()); + + assert is#nil(nil()); + + assert is#node(leaf()); } \ No newline at end of file -- cgit v1.2.3