From ed24180cd004e941ac619f9fb98a260fa3cd84a1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 10 Dec 2025 08:02:06 -0800 Subject: [PATCH] KNOWNBUG test for SMV's process --- regression/smv/process/process1.desc | 9 +++++++++ regression/smv/process/process1.smv | 9 +++++++++ 2 files changed, 18 insertions(+) create mode 100644 regression/smv/process/process1.desc create mode 100644 regression/smv/process/process1.smv diff --git a/regression/smv/process/process1.desc b/regression/smv/process/process1.desc new file mode 100644 index 000000000..55a48b851 --- /dev/null +++ b/regression/smv/process/process1.desc @@ -0,0 +1,9 @@ +KNOWNBUG +process1.smv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This does not parse. diff --git a/regression/smv/process/process1.smv b/regression/smv/process/process1.smv new file mode 100644 index 000000000..bd99854ef --- /dev/null +++ b/regression/smv/process/process1.smv @@ -0,0 +1,9 @@ +-- from the NuSMV 2.7 manual + +MODULE my_module + -- my module definition... + +MODULE main + VAR + p1 : process my_module; + p2 : process my_module;