From c9be27f412699c2ff6323738ec7d3d6bcb91fcdd Mon Sep 17 00:00:00 2001 From: David Deharbe Date: Wed, 11 Mar 2026 14:48:00 +0000 Subject: [PATCH] update following [] rewrite move downstream pog [#81070] --- extern/BAST | 2 +- test/CMakeLists.txt | 1 + test/input/emptyseq_1/emptyseq_1.mch | 8 ++ test/input/emptyseq_1/input.pog | 88 +++++++++++++++++++++ test/output/reference/emptyseq_1/exitcode | 1 + test/output/reference/emptyseq_1/output.pog | 87 ++++++++++++++++++++ test/output/reference/emptyseq_1/stderr | 0 7 files changed, 186 insertions(+), 1 deletion(-) create mode 100644 test/input/emptyseq_1/emptyseq_1.mch create mode 100644 test/input/emptyseq_1/input.pog create mode 100644 test/output/reference/emptyseq_1/exitcode create mode 100644 test/output/reference/emptyseq_1/output.pog create mode 100644 test/output/reference/emptyseq_1/stderr diff --git a/extern/BAST b/extern/BAST index 07ec7e5..ef0a47a 160000 --- a/extern/BAST +++ b/extern/BAST @@ -1 +1 @@ -Subproject commit 07ec7e5d61372aa4305c48275c33d2079b594a2a +Subproject commit ef0a47a30c836b430b76d6ac5b1204b158323e22 diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index e074634..310d639 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -18,3 +18,4 @@ macro(add_pog_test id) endmacro(add_pog_test) # add_pog_test(empty_1) +# add_pog_test(emptyseq_1) diff --git a/test/input/emptyseq_1/emptyseq_1.mch b/test/input/emptyseq_1/emptyseq_1.mch new file mode 100644 index 0000000..1f49716 --- /dev/null +++ b/test/input/emptyseq_1/emptyseq_1.mch @@ -0,0 +1,8 @@ +MACHINE emptyseq_1 +ABSTRACT_CONSTANTS + empty_seq +PROPERTIES + empty_seq : seq(INTEGER ) +ASSERTIONS + empty_seq = [] +END diff --git a/test/input/emptyseq_1/input.pog b/test/input/emptyseq_1/input.pog new file mode 100644 index 0000000..f0c660a --- /dev/null +++ b/test/input/emptyseq_1/input.pog @@ -0,0 +1,88 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + AssertionLemmas + + + + + + + + + + Assertion is verified + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/test/output/reference/emptyseq_1/exitcode b/test/output/reference/emptyseq_1/exitcode new file mode 100644 index 0000000..573541a --- /dev/null +++ b/test/output/reference/emptyseq_1/exitcode @@ -0,0 +1 @@ +0 diff --git a/test/output/reference/emptyseq_1/output.pog b/test/output/reference/emptyseq_1/output.pog new file mode 100644 index 0000000..abd15b5 --- /dev/null +++ b/test/output/reference/emptyseq_1/output.pog @@ -0,0 +1,87 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + AssertionLemmas + + + + + + + + + + Assertion is verified + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/test/output/reference/emptyseq_1/stderr b/test/output/reference/emptyseq_1/stderr new file mode 100644 index 0000000..e69de29