Merge pull request #1235 from diffblue/sva-empty-sequence-buechi

SVA->Buechi: empty sequences

Author: tautschnig

regression/ebmc-spot/sva-buechi/followed-by5.bdd.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/followed-by5.sv
 --buechi --bdd
 ^\[main\.p0\] \(1 \[\*0\]\) #=# main\.x == 0: PROVED$
@@ -8,4 +8,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-Empty LHS sequences are not implemented.

regression/ebmc-spot/sva-buechi/followed-by5.bmc.desc

@@ -1,11 +1,10 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/followed-by5.sv
 --buechi --bound 2
-^\[main\.p0\] \(1 \[\*0\]\) #=# main\.x == 0: PROVED$
+^\[main\.p0\] \(1 \[\*0\]\) #=# main\.x == 0: PROVED up to bound 2$
 ^\[main\.p1\] \(1 \[\*0\]\) #-# 1: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Empty LHS sequences are not implemented.

src/temporal-logic/ltl_sva_to_string.cpp

@@ -14,7 +14,6 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <verilog/sva_expr.h>
 
 #include "ltl.h"
-#include "rewrite_sva_sequence.h"
 #include "temporal_expr.h"
 #include "temporal_logic.h"
 
@@ -304,11 +303,8 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   {
     PRECONDITION(mode == PROPERTY);
     auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
+    auto op_rec = rec(sequence, SVA_SEQUENCE);
 
-    // re-write to get rid of empty matches
-    auto sequence_rewritten = rewrite_sva_sequence(sequence);
-
-    auto op_rec = rec(sequence_rewritten, SVA_SEQUENCE);
     // weak closure
     return resultt{precedencet::ATOM, '{' + op_rec.s + '}'};
   }
@@ -456,8 +452,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     }
     else if(repetition.is_empty_match())
     {
-      // handled by rewite_sva_sequence
-      return resultt{precedencet::ATOM, "0"};
+      return resultt{precedencet::ATOM, "[*0]"};
     }
     else if(repetition.is_singleton())
     {