diff --git a/Test/datatypes/is-cons.bpl b/Test/datatypes/is-cons.bpl new file mode 100644 index 000000000..ced4e462b --- /dev/null +++ b/Test/datatypes/is-cons.bpl @@ -0,0 +1,12 @@ +// RUN: %parallel-boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +datatype X { + A'(a: int), + B'(b: bool) +} + +procedure P(x: X) { + assume x is A'; + assert !(x is B'); +} diff --git a/Test/datatypes/is-cons.bpl.expect b/Test/datatypes/is-cons.bpl.expect new file mode 100644 index 000000000..37fad75c9 --- /dev/null +++ b/Test/datatypes/is-cons.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors