Merge pull request #1158 from diffblue/followed-by5.bmc-fix

word-level BMC: fix `#-#` and `#=#` for empty matches

Author: tautschnig

CHANGELOG

@@ -3,6 +3,7 @@
 * Verilog: `elsif preprocessor directive
 * Verilog: fix for named generate blocks
 * Verilog: $onehot and $onehot0 are now elaboration-time constant
+* SystemVerilog: fix for #-# and #=# for empty matches
 * LTL/SVA to Buechi with --buechi
 
 # EBMC 5.6

regression/verilog/SVA/followed-by5.bmc.desc

@@ -1,11 +1,10 @@
-KNOWNBUG
+CORE
 followed-by5.sv
 --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/trans-word-level/property.cpp

@@ -644,7 +644,7 @@ static obligationst property_obligations_rec(
     // the result is a property expression.
     auto &followed_by = to_sva_followed_by_expr(property_expr);
 
-    // get (proper) match points for LHS sequence
+    // get match points for LHS sequence
     auto matches = instantiate_sequence(
       followed_by.antecedent(),
       sva_sequence_semanticst::STRONG,
@@ -656,10 +656,20 @@ static obligationst property_obligations_rec(
 
     for(auto &match : matches)
     {
+      bool overlapped = property_expr.id() == ID_sva_overlapped_followed_by;
+
+      // empty match?
+      if(match.empty_match() && overlapped)
+      {
+        // won't yield a disjunct
+        continue;
+      }
+
       mp_integer property_start = match.end_time;
 
-      // #=# advances the clock by one from the sequence match point
-      if(property_expr.id() == ID_sva_nonoverlapped_followed_by)
+      // #=# advances the clock by one from the sequence match point,
+      // unless the LHS is an empty match.
+      if(!match.empty_match() && !overlapped)
         property_start += 1;
 
       // at the end?