From 9f312f0135fd54d9c71c60bc856a48318bd632d3 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Wed, 19 Jul 2017 17:02:57 +0200 Subject: 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. --- data/property/combinational_processes.pro | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'data/property/combinational_processes.pro') 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)) + ) ) ) ) -- cgit v1.2.3-70-g09d2