fx

Author: kroening

regression/ebmc/sva-monitor/s_nexttime1.desc

@@ -2,12 +2,12 @@ CORE
 s_nexttime1.sv
 --sva-monitor --smv-word-level
 ^VAR initial : boolean;$
-^VAR nexttime_activated : boolean;$
+^VAR delayed_active : boolean;$
 ^INIT sva-monitor::initial$
-^INIT !sva-monitor::nexttime_activated$
+^INIT !sva-monitor::delayed_active$
 ^TRANS !next\(sva-monitor::initial\)$
-^TRANS next\(sva-monitor::nexttime_activated\) = sva-monitor::initial$
-^LTLSPEC G \(sva-monitor::nexttime_activated -> FALSE\)$
+^TRANS next\(sva-monitor::delayed_active\) = sva-monitor::initial$
+^LTLSPEC G \(sva-monitor::delayed_active -> FALSE\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --