Buechi: identify special cases where reachability is sufficient

This adds treatment for the special case where all nonaccepting states of
the Buechi automaton have an unconditional self-loop.

In this case, when these nonaccepting states is reached, the trace cannot be
extended to an accepting trace, and will hence be rejected.

Hence, in this case, the Buechi acceptance condition is unnecessary, and a
simple reachability property is sufficient.

Author: kroening

regression/ebmc-spot/sva-buechi/sequence5.desc

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sequence5.sv
 --buechi
-^\[main\.p0\] 1: PROVED up to bound \d+$
+^\[main\.p0\] 1: PROVED \(1-induction\)$
 ^\[main\.p1\] 0: REFUTED$
 ^\[main\.p2\] 1'bx: REFUTED$
 ^\[main\.p3\] 1'bz: REFUTED$

regression/ebmc-spot/sva-buechi/sva_and1.desc

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sva_and1.sv
 --buechi
-^\[main\.p0\] always \(1 and 1\): PROVED up to bound \d+$
+^\[main\.p0\] always \(1 and 1\): PROVED \(1-induction\)$
 ^\[main\.p1\] always \(1 and 0\): REFUTED$
 ^\[main\.p2\] always \(1 and 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

regression/ebmc-spot/sva-buechi/sva_iff1.desc

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sva_iff1.sv
 --buechi
-^\[main\.p0\] always \(1 iff 1\): PROVED up to bound \d+$
+^\[main\.p0\] always \(1 iff 1\): PROVED \(1-induction\)$
 ^\[main\.p1\] always \(1 iff 0\): REFUTED$
 ^\[main\.p2\] always \(1 iff 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

regression/ebmc-spot/sva-buechi/sva_implies1.desc

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sva_implies1.sv
 --buechi
-^\[main\.p0\] always \(1 implies 1\): PROVED up to bound \d+$
+^\[main\.p0\] always \(1 implies 1\): PROVED \(1-induction\)$
 ^\[main\.p1\] always \(1 implies 0\): REFUTED$
 ^\[main\.p2\] always \(1 implies 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

regression/ebmc-spot/sva-buechi/sva_not1.desc

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sva_not1.sv
 --buechi
-^\[main\.p0] always not 0: PROVED up to bound \d+$
+^\[main\.p0] always not 0: PROVED \(1-induction\)$
 ^\[main\.p1] always not 1: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$

src/ebmc/instrument_buechi.cpp

@@ -64,15 +64,24 @@ void instrument_buechi(
     transition_system.trans_expr.trans() =
       and_exprt{transition_system.trans_expr.trans(), buechi.trans};
 
-    // Replace the normalized property expression.
-    // Note that we have negated the property,
-    // so this is the negation of the Buechi acceptance condition.
-    property.normalized_expr =
-      F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}};
+    // Replace the normalized property expression
+    // by the Buechi acceptance condition.
+    exprt::operandst property_conjuncts;
+
+    if(!buechi.liveness_signal.is_false())
+    {
+      // Note that we have negated the property,
+      // so this is the negation of the Buechi acceptance condition.
+      property_conjuncts.push_back(
+        F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}});
+    }
 
     if(!buechi.error_signal.is_true())
-      property.normalized_expr = and_exprt{
-        property.normalized_expr, G_exprt{not_exprt{buechi.error_signal}}};
+    {
+      property_conjuncts.push_back(G_exprt{not_exprt{buechi.error_signal}});
+    }
+
+    property.normalized_expr = conjunction(property_conjuncts);
 
     message.debug() << "New property: " << format(property.normalized_expr)
                     << messaget::eom;