From 2d5d97ef115f2719ed0ac0413a05da944e3df225 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 14 Jul 2025 14:16:53 -0700
Subject: [PATCH] SMV: test for LTL property with 'or'

This adds a test for an LTL property with a top-level 'or'.
---
 regression/smv/LTL/smv_ltlspec_or1.desc | 8 ++++++++
 regression/smv/LTL/smv_ltlspec_or1.smv  | 5 +++++
 2 files changed, 13 insertions(+)
 create mode 100644 regression/smv/LTL/smv_ltlspec_or1.desc
 create mode 100644 regression/smv/LTL/smv_ltlspec_or1.smv

diff --git a/regression/smv/LTL/smv_ltlspec_or1.desc b/regression/smv/LTL/smv_ltlspec_or1.desc
new file mode 100644
index 000000000..f097f716c
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_or1.desc
@@ -0,0 +1,8 @@
+CORE
+smv_ltlspec_or1.smv
+--bound 10
+^\[spec1\] F !x \| G x: PROVED up to bound 10$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/LTL/smv_ltlspec_or1.smv b/regression/smv/LTL/smv_ltlspec_or1.smv
new file mode 100644
index 000000000..a9148a080
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_or1.smv
@@ -0,0 +1,5 @@
+MODULE main
+
+VAR x : boolean;
+
+LTLSPEC (F !x) | G x