aboutsummaryrefslogtreecommitdiff
path: root/examples/tll/tll_strict.vnnlib
diff options
context:
space:
mode:
Diffstat (limited to 'examples/tll/tll_strict.vnnlib')
-rw-r--r--examples/tll/tll_strict.vnnlib16
1 files changed, 0 insertions, 16 deletions
diff --git a/examples/tll/tll_strict.vnnlib b/examples/tll/tll_strict.vnnlib
deleted file mode 100644
index 0079b1e..0000000
--- a/examples/tll/tll_strict.vnnlib
+++ /dev/null
@@ -1,16 +0,0 @@
-; Strict Equivalence for TLL
-
-; Constant declaration
-(declare-const X_0 Real)
-(declare-const X_1 Real)
-(declare-const Y_0 Real)
-(declare-const Y_1 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 strict equivalence
-(assert (not (= Y_0 Y_1)))