From 81d4d604aa43660b732b3538734a52d509d7c5df Mon Sep 17 00:00:00 2001
From: ericmarin <maarin.eric@gmail.com>
Date: Tue, 31 Mar 2026 16:43:47 +0200
Subject: refactored examples

---
 examples/pendulum/pendulum_argmax.vnnlib | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 examples/pendulum/pendulum_argmax.vnnlib

(limited to 'examples/pendulum/pendulum_argmax.vnnlib')

diff --git a/examples/pendulum/pendulum_argmax.vnnlib b/examples/pendulum/pendulum_argmax.vnnlib
new file mode 100644
index 0000000..c11dc0b
--- /dev/null
+++ b/examples/pendulum/pendulum_argmax.vnnlib
@@ -0,0 +1,27 @@
+; Argmax Equivalence for Pendulum
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+
+; Violation of argmax equivalence
+(assert (or
+  (and 
+    (> Y_0 Y_1)
+		(> Y_3 Y_2)
+  )
+  (and 
+    (> Y_1 Y_0)
+		(> Y_2 Y_3)
+  )
+))
-- 
cgit v1.2.3