Test combination of k-induction and Buechi instrumentation

This adds tests for the combination of k-induction and Buechi
instrumentation.

Author: kroening

regression/ebmc-spot/sva-buechi/cycle_delay2.desc renamed to regression/ebmc-spot/sva-buechi/cycle_delay2.bmc.desc

@@ -0,0 +1,7 @@
+CORE
+../../verilog/SVA/cycle_delay2.sv
+--buechi --k-induction --bound 3
+^\[.*\] ##\[1:2\] main\.x == 2: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc-spot/sva-buechi/cycle_delay2.k.desc

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/empty_sequence1.sv
+--buechi --k-induction --bound 1
+^\[main\.p0\] 1 \[\*0\]: REFUTED$
+^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: PROVED$
+^\[main\.p2\] main\.x == 0 ##1 \(1 \[\*0\]\): PROVED$
+^\[main\.p3\] \(1 \[\*0\]\) ##0 1: REFUTED$
+^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/empty_sequence1.k.desc

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/eventually1.sv
+--buechi --k-induction --bound 2
+^\[main\.p0\] always \(main\.counter == 1 implies \(eventually \[1:2\] main\.counter == 3\)\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc-spot/sva-buechi/eventually1.desc renamed to regression/ebmc-spot/sva-buechi/eventually1.bmc.desc

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/eventually4.sv
+--buechi --k-induction --bound 1
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/eventually1.k.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/followed-by1.sv
+--buechi --k-induction --bound 1
+^\[main\.p0\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): PROVED$
+^\[main\.p1\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/eventually4.desc renamed to regression/ebmc-spot/sva-buechi/eventually4.bmc.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/followed-by2.sv
+--buechi --k-induction --bound 1
+^\[main\.p0\] always \(\(main\.a #-# main\.b\) iff \(not \(main\.a |-> \(not main\.b\)\)\)\): PROVED$
+^\[main\.p1\] always \(\(main\.a #=# main\.b\) iff \(not \(main\.a |=> \(not main\.b\)\)\)\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/eventually4.k.desc

@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/followed-by4.sv
+--buechi --k-induction --bound 3
+^\[main\.p1\] always \(main\.x == 0 #-# 1\): REFUTED$
+^\[main\.p2\] \(1 or \(##2 1\)\) #-# main\.x == 2: PROVED$
+^\[main\.p3\] \(1 or \(##2 1\)\) #-# main\.x == 0: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--