Formula.and(Formula...) != a.and(Formula...)

Having both a static and a non-static function share a name does not
seem like a sane decision.

1 files changed, 7 insertions, 7 deletions

diff --git a/data/property/combinational_processes.pro b/data/property/combinational_processes.pro
index 7f8405f..5008a06 100644
--- a/data/property/combinational_processes.pro
+++ b/data/property/combinational_processes.pro
@@ -4,12 +4,6 @@
    )
    (forall sl1 waveform
       (and
-         (CTL_verifies ps
-            (implies
-               (EF (expr_writes sl1))
-               (AF (expr_writes sl1))
-            )
-         )
          (implies
             (exists target waveform
                (CTL_verifies ps
@@ -28,7 +22,13 @@
                   )
                )
             )
-            (is_in_sensitivity_list ps sl1)
+            (is_in_sensitivity_list sl1 ps)
+         )
+         (CTL_verifies ps
+            (implies
+               (EF (expr_writes sl1))
+               (AF (expr_writes sl1))
+            )
          )
       )
    )