Merge pull request #1025 from diffblue/fix-sva_s_always

Bugfix: `s_always` is a temporal logic operator

Author: tautschnig

regression/verilog/SVA/initial1.desc

@@ -5,7 +5,7 @@ initial1.sv
 ^\[main\.p1\] main\.counter == 100: REFUTED$
 ^\[main\.p2\] ##1 main\.counter == 1: PROVED up to bound 5$
 ^\[main\.p3\] ##1 main\.counter == 100: REFUTED$
-^\[main\.p4\] s_nexttime main\.counter == 1: PROVED$
+^\[main\.p4\] s_nexttime main\.counter == 1: PROVED up to bound 5$
 ^EXIT=10$
 ^SIGNAL=0$
 --

src/temporal-logic/temporal_logic.cpp

@@ -117,13 +117,14 @@ bool is_SVA_operator(const exprt &expr)
   return is_SVA_sequence(expr) || id == ID_sva_disable_iff ||
          id == ID_sva_accept_on || id == ID_sva_reject_on ||
          id == ID_sva_sync_accept_on || id == ID_sva_sync_reject_on ||
-         id == ID_sva_always || id == ID_sva_ranged_always ||
-         id == ID_sva_nexttime || id == ID_sva_s_nexttime ||
-         id == ID_sva_indexed_nexttime || id == ID_sva_until ||
-         id == ID_sva_s_until || id == ID_sva_until_with ||
-         id == ID_sva_s_until_with || id == ID_sva_eventually ||
-         id == ID_sva_s_eventually || id == ID_sva_ranged_s_eventually ||
-         id == ID_sva_cycle_delay || id == ID_sva_overlapped_followed_by ||
+         id == ID_sva_always || id == ID_sva_s_always ||
+         id == ID_sva_ranged_always || id == ID_sva_nexttime ||
+         id == ID_sva_s_nexttime || id == ID_sva_indexed_nexttime ||
+         id == ID_sva_until || id == ID_sva_s_until ||
+         id == ID_sva_until_with || id == ID_sva_s_until_with ||
+         id == ID_sva_eventually || id == ID_sva_s_eventually ||
+         id == ID_sva_ranged_s_eventually || id == ID_sva_cycle_delay ||
+         id == ID_sva_overlapped_followed_by ||
          id == ID_sva_nonoverlapped_followed_by;
 }