Merge pull request #1127 from diffblue/proof-via

EBMC: show proof engine in result

Author: tautschnig

regression/ebmc/engine-heuristic/basic2.desc

@@ -3,7 +3,7 @@ basic2.sv
 
 ^\[main\.a0\] always not s_eventually !main\.y: UNSUPPORTED: unsupported by k-induction$
 ^\[main\.a1\] always !main\.x: ASSUMED$
-^\[main\.p0\] always !main\.z: PROVED$
+^\[main\.p0\] always !main\.z: PROVED \(1-induction\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc/example1/test.desc

@@ -1,6 +1,6 @@
 CORE
 example1.sv
 
-^\[.*\] always 2'\(main\.a\) \+ main\.b == main\.result: PROVED$
+^\[.*\] always 2'\(main\.a\) \+ main\.b == main\.result: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$

regression/smv/enums/enum1.desc

@@ -1,7 +1,7 @@
 CORE broken-smt-backend
 enum1.smv
 
-^\[.*\] AG some_var != off: PROVED$
+^\[.*\] AG some_var != off: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/expressions/smv_if2.desc

@@ -1,7 +1,7 @@
 CORE
 smv_if2.smv
 
-^\[.*\] X \(b = 2 \| b = 4\): PROVED$
+^\[.*\] X \(b = 2 \| b = 4\): PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/expressions/xnor1.desc

@@ -1,7 +1,7 @@
 CORE
 xnor1.smv
 
-^\[spec1\] G x: PROVED$
+^\[spec1\] G x: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/smv/initial1.desc

@@ -1,7 +1,7 @@
 CORE
 initial1.smv
 
-^\[spec1\] tmp1 = TRUE: PROVED$
+^\[spec1\] tmp1 = TRUE: PROVED .*$
 ^\[spec2\] tmp2 = TRUE: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/smv/word/bitwise1.desc

@@ -1,13 +1,13 @@
 CORE
 bitwise1.smv
 
-^\[.*\] !\(0ud8_123 = 0ud8_132\): PROVED$
-^\[.*\] !\(0sd8_123 = -0sd8_124\): PROVED$
-^\[.*\] \(0ud8_123 \& 0ud8_7\) = 0ud8_3: PROVED$
-^\[.*\] \(0ud8_123 \| 0ud8_7\) = 0ud8_127: PROVED$
-^\[.*\] \(0ud8_123 xor 0ud8_7\) = 0ud8_124: PROVED$
-^\[.*\] \(0ud8_123 xnor 0ud8_7\) = 0ud8_131: PROVED$
-^\[.*\] \(0ud8_123 <-> 0ud8_7\) = 0ud8_131: PROVED$
+^\[.*\] !\(0ud8_123 = 0ud8_132\): PROVED .*$
+^\[.*\] !\(0sd8_123 = -0sd8_124\): PROVED .*$
+^\[.*\] \(0ud8_123 \& 0ud8_7\) = 0ud8_3: PROVED .*$
+^\[.*\] \(0ud8_123 \| 0ud8_7\) = 0ud8_127: PROVED .*$
+^\[.*\] \(0ud8_123 xor 0ud8_7\) = 0ud8_124: PROVED .*$
+^\[.*\] \(0ud8_123 xnor 0ud8_7\) = 0ud8_131: PROVED .*$
+^\[.*\] \(0ud8_123 <-> 0ud8_7\) = 0ud8_131: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/word/concat1.desc

@@ -1,9 +1,9 @@
 CORE
 concat1.smv
 
-^\[.*\] 0ud8_123 :: 0ud8_1 = 0ud16_31489: PROVED$
-^\[.*\] 0sd8_123 :: 0sd8_1 = 0ud16_31489: PROVED$
-^\[.*\] 0sd8_123 :: 0ud8_1 = 0ud16_31489: PROVED$
+^\[.*\] 0ud8_123 :: 0ud8_1 = 0ud16_31489: PROVED .*$
+^\[.*\] 0sd8_123 :: 0sd8_1 = 0ud16_31489: PROVED .*$
+^\[.*\] 0sd8_123 :: 0ud8_1 = 0ud16_31489: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/word/extend1.desc

@@ -1,8 +1,8 @@
 CORE
 extend1.smv
 
-^\[p0\] extend\(0ud1_1, 7\) = 0ud8_1: PROVED$
-^\[p1\] extend\(-0sd1_1, 7\) = -0sd8_1: PROVED$
+^\[p0\] extend\(0ud1_1, 7\) = 0ud8_1: PROVED .*$
+^\[p1\] extend\(-0sd1_1, 7\) = -0sd8_1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/word/resize1.desc

@@ -1,8 +1,8 @@
 CORE
 resize1.smv
 
-^\[p0\] resize\(0ud1_1, 8\) = 0ud8_1: PROVED$
-^\[p1\] resize\(-0sd1_1, 1\) = -0sd1_1: PROVED$
+^\[p0\] resize\(0ud1_1, 8\) = 0ud8_1: PROVED .*$
+^\[p1\] resize\(-0sd1_1, 1\) = -0sd1_1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/word/shift1.desc

@@ -1,18 +1,18 @@
 CORE
 shift1.smv
 
-^\[.*\] 0ud8_123 >> 0 = 0ud8_123: PROVED$
-^\[.*\] 0ud8_123 >> 1 = 0ud8_61: PROVED$
-^\[.*\] 0ud8_123 >> 8 = 0ud8_0: PROVED$
-^\[.*\] 0ud8_123 << 0 = 0ud8_123: PROVED$
-^\[.*\] 0ud8_123 << 1 = 0ud8_246: PROVED$
-^\[.*\] 0ud8_123 << 2 = 0ud8_236: PROVED$
-^\[.*\] 0sd8_123 >> 0 = 0sd8_123: PROVED$
-^\[.*\] 0sd8_123 >> 1 = 0sd8_61: PROVED$
-^\[.*\] 0sd8_123 >> 8 = 0sd8_0: PROVED$
-^\[.*\] 0sd8_123 << 0 = 0sd8_123: PROVED$
-^\[.*\] 0sd8_123 << 1 = -0sd8_10: PROVED$
-^\[.*\] 0sd8_123 << 2 = -0sd8_20: PROVED$
+^\[.*\] 0ud8_123 >> 0 = 0ud8_123: PROVED .*$
+^\[.*\] 0ud8_123 >> 1 = 0ud8_61: PROVED .*$
+^\[.*\] 0ud8_123 >> 8 = 0ud8_0: PROVED .*$
+^\[.*\] 0ud8_123 << 0 = 0ud8_123: PROVED .*$
+^\[.*\] 0ud8_123 << 1 = 0ud8_246: PROVED .*$
+^\[.*\] 0ud8_123 << 2 = 0ud8_236: PROVED .*$
+^\[.*\] 0sd8_123 >> 0 = 0sd8_123: PROVED .*$
+^\[.*\] 0sd8_123 >> 1 = 0sd8_61: PROVED .*$
+^\[.*\] 0sd8_123 >> 8 = 0sd8_0: PROVED .*$
+^\[.*\] 0sd8_123 << 0 = 0sd8_123: PROVED .*$
+^\[.*\] 0sd8_123 << 1 = -0sd8_10: PROVED .*$
+^\[.*\] 0sd8_123 << 2 = -0sd8_20: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/word/signed1.desc

@@ -1,7 +1,7 @@
 CORE
 signed1.smv
 
-^\[p0\] signed\(0ud1_1\) = -0sd1_1: PROVED$
+^\[p0\] signed\(0ud1_1\) = -0sd1_1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/word/unsigned1.desc

@@ -1,7 +1,7 @@
 CORE
 unsigned1.smv
 
-^\[p0\] unsigned\(-0sd1_1\) = 0ud1_1: PROVED$
+^\[p0\] unsigned\(-0sd1_1\) = 0ud1_1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/immediate2.desc

@@ -2,7 +2,7 @@ CORE
 immediate2.sv
 
 ^\[main\.assume\.1\] assume always 0: ASSUMED$
-^\[main\.assert\.2\] always main\.index < 10: PROVED$
+^\[main\.assert\.2\] always main\.index < 10: PROVED .*$
 ^\[main\.assert\.3\] always 0: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/verilog/SVA/immediate3.desc

@@ -1,7 +1,7 @@
 CORE
 immediate3.sv
 
-^\[full_adder\.assert\.1\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED$
+^\[full_adder\.assert\.1\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/initial1.bmc.desc

@@ -1,12 +1,12 @@
 CORE
 initial1.sv
 --module main
-^\[main\.p0\] main\.counter == 0: PROVED$
+^\[main\.p0\] main\.counter == 0: PROVED .*$
 ^\[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\.p5\] always \[1:1\] main\.counter == 1: PROVED$
+^\[main\.p4\] s_nexttime main\.counter == 1: PROVED .*$
+^\[main\.p5\] always \[1:1\] main\.counter == 1: PROVED .*$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/SVA/initial2.desc

@@ -1,8 +1,8 @@
 CORE
 initial2.sv
 --module main
-^\[main\.assert\.1\] main\.counter == 1: PROVED$
-^\[main\.assert\.2\] main\.counter == 2: PROVED$
+^\[main\.assert\.1\] main\.counter == 1: PROVED .*$
+^\[main\.assert\.2\] main\.counter == 2: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence5.desc

@@ -1,7 +1,7 @@
 CORE
 sequence5.sv
 
-^\[main\.p0\] 1: PROVED$
+^\[main\.p0\] 1: PROVED .*$
 ^\[main\.p1\] 0: REFUTED$
 ^\[main\.p2\] 1'bx: REFUTED$
 ^\[main\.p3\] 1'bz: REFUTED$

regression/verilog/SVA/sequence_or1.bmc.desc

@@ -1,8 +1,8 @@
 CORE
 sequence_or1.sv
 
-^\[main\.p0\] main\.x == 0 or main\.x == 1: PROVED$
-^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED$
+^\[main\.p0\] main\.x == 0 or main\.x == 1: PROVED .*$
+^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED .*$
 ^\[main\.p2\] main\.x == 0 or \(nexttime main\.x == 1\): PROVED up to bound \d+$
 ^\[main\.p3\] \(nexttime main\.x == 1\) or main\.x == 1: PROVED up to bound \d+$
 ^\[main\.p4\] \(main\.x == 0 or main\.x != 10\) |=> main\.x == 1: PROVED up to bound \d+$

regression/verilog/SVA/static_final1.desc

@@ -1,7 +1,7 @@
 CORE
 static_final1.sv
 
-^\[full_adder\.p0\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED$
+^\[full_adder\.p0\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sva_and1.desc

@@ -1,7 +1,7 @@
 CORE
 sva_and1.sv
 
-^\[main\.p0\] always \(1 and 1\): PROVED$
+^\[main\.p0\] always \(1 and 1\): PROVED .*$
 ^\[main\.p1\] always \(1 and 0\): REFUTED$
 ^\[main\.p2\] always \(1 and 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

regression/verilog/SVA/sva_iff1.desc

@@ -1,7 +1,7 @@
 CORE
 sva_iff1.sv
 
-^\[main\.p0\] always \(1 iff 1\): PROVED$
+^\[main\.p0\] always \(1 iff 1\): PROVED .*$
 ^\[main\.p1\] always \(1 iff 0\): REFUTED$
 ^\[main\.p2\] always \(1 iff 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

regression/verilog/SVA/sva_implies1.desc

@@ -1,7 +1,7 @@
 CORE
 sva_implies1.sv
 
-^\[main\.p0\] always \(1 implies 1\): PROVED$
+^\[main\.p0\] always \(1 implies 1\): PROVED .*$
 ^\[main\.p1\] always \(1 implies 0\): REFUTED$
 ^\[main\.p2\] always \(1 implies 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

regression/verilog/case/nested_case1.desc

@@ -3,6 +3,6 @@ nested_case1.v
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.property.p1\] .* PROVED$
+^\[main.property.p1\] .* PROVED .*$
 --
 ^warning: ignoring

regression/verilog/case/riscv-alu.desc

@@ -1,16 +1,16 @@
 CORE
 riscv-alu.sv
 --module alu
-^\[alu\.pADD\] always alu\.op == \{ 7'b0000000, 3'b000 \} -> alu\.out == alu\.a \+ alu\.b: PROVED$
-^\[alu\.pSUB\] always alu\.op == \{ 7'b0100000, 3'b000 \} -> alu\.out == alu\.a - alu\.b: PROVED$
-^\[alu\.pSLL\] always alu\.op == \{ 7'b0000000, 3'b001 \} -> alu\.out == alu\.a << alu\.b\[4:0\]: PROVED$
-^\[alu\.pSLT\] always alu\.op == \{ 7'b0000000, 3'b010 \} -> alu\.out == \$signed\(alu\.a\) < \$signed\(alu\.b\): PROVED$
-^\[alu\.pSLTU\] always alu\.op == \{ 7'b0000000, 3'b011 \} -> alu\.out == alu\.a < alu\.b: PROVED$
-^\[alu\.pXOR\] always alu\.op == \{ 7'b0000000, 3'b100 \} -> alu\.out == \(alu\.a \^ alu\.b\): PROVED$
-^\[alu\.pSRL\] always alu\.op == \{ 7'b0000000, 3'b101 \} -> alu\.out == alu\.a >> alu\.b\[4:0\]: PROVED$
-^\[alu\.pSRA\] always alu\.op == \{ 7'b0100000, 3'b101 \} -> alu\.out == \$signed\(alu\.a\) >>> alu\.b\[4:0\]: PROVED$
-^\[alu\.pOR\] always alu\.op == \{ 7'b0000000, 3'b110 \} -> alu\.out == \(alu\.a | alu\.b\): PROVED$
-^\[alu\.pAND\] always alu\.op == \{ 7'b0000000, 3'b111 \} -> alu\.out == \(alu\.a & alu\.b\): PROVED$
+^\[alu\.pADD\] always alu\.op == \{ 7'b0000000, 3'b000 \} -> alu\.out == alu\.a \+ alu\.b: PROVED .*$
+^\[alu\.pSUB\] always alu\.op == \{ 7'b0100000, 3'b000 \} -> alu\.out == alu\.a - alu\.b: PROVED .*$
+^\[alu\.pSLL\] always alu\.op == \{ 7'b0000000, 3'b001 \} -> alu\.out == alu\.a << alu\.b\[4:0\]: PROVED .*$
+^\[alu\.pSLT\] always alu\.op == \{ 7'b0000000, 3'b010 \} -> alu\.out == \$signed\(alu\.a\) < \$signed\(alu\.b\): PROVED .*$
+^\[alu\.pSLTU\] always alu\.op == \{ 7'b0000000, 3'b011 \} -> alu\.out == alu\.a < alu\.b: PROVED .*$
+^\[alu\.pXOR\] always alu\.op == \{ 7'b0000000, 3'b100 \} -> alu\.out == \(alu\.a \^ alu\.b\): PROVED .*$
+^\[alu\.pSRL\] always alu\.op == \{ 7'b0000000, 3'b101 \} -> alu\.out == alu\.a >> alu\.b\[4:0\]: PROVED .*$
+^\[alu\.pSRA\] always alu\.op == \{ 7'b0100000, 3'b101 \} -> alu\.out == \$signed\(alu\.a\) >>> alu\.b\[4:0\]: PROVED .*$
+^\[alu\.pOR\] always alu\.op == \{ 7'b0000000, 3'b110 \} -> alu\.out == \(alu\.a | alu\.b\): PROVED .*$
+^\[alu\.pAND\] always alu\.op == \{ 7'b0000000, 3'b111 \} -> alu\.out == \(alu\.a & alu\.b\): PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/data-types/chandle1.desc

@@ -1,8 +1,8 @@
 CORE
 chandle1.sv
 
-^\[main\.p0\] always main\.some_handle == null: PROVED$
-^\[main\.p1\] always \$typename\(main\.some_handle\) == "chandle": PROVED$
+^\[main\.p0\] always main\.some_handle == null: PROVED .*$
+^\[main\.p1\] always \$typename\(main\.some_handle\) == "chandle": PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/data-types/vector_types2.desc

@@ -1,7 +1,7 @@
 CORE
 vector_types2.sv
 
-^\[.*\] always \$bits\(main\.x\) == \(1 << main\.p\) \+ 1: PROVED$
+^\[.*\] always \$bits\(main\.x\) == \(1 << main\.p\) \+ 1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/enums/enum4.desc

@@ -3,5 +3,5 @@ enum4.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.p1\] always main\.A == \[7:0\]'\(1\): PROVED$
+^\[main\.p1\] always main\.A == \[7:0\]'\(1\): PROVED .*$
 --

regression/verilog/enums/enum_base_type1.desc

@@ -3,5 +3,5 @@ enum_base_type1.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\[.*\] always \$bits\(main\.A\) == 8: PROVED$
+^\[.*\] always \$bits\(main\.A\) == 8: PROVED .*$
 --

regression/verilog/enums/enum_base_type2.desc

@@ -3,5 +3,5 @@ enum_base_type2.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\[.*\] always \$bits\(main\.A\) == main\.p: PROVED$
+^\[.*\] always \$bits\(main\.A\) == main\.p: PROVED .*$
 --

regression/verilog/enums/enum_cast1.desc

@@ -3,6 +3,6 @@ enum_cast1.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.p1\] always main.A == signed \[31:0\]'\(1\): PROVED$
-^\[main\.p2\] always main.B == signed \[31:0\]'\(2\): PROVED$
+^\[main\.p1\] always main.A == signed \[31:0\]'\(1\): PROVED .*$
+^\[main\.p2\] always main.B == signed \[31:0\]'\(2\): PROVED .*$
 --

regression/verilog/enums/enum_initializers1.desc

@@ -1,8 +1,8 @@
 CORE
 enum_initializers1.sv
 
-^\[main\.pA\] always main.A == 1: PROVED$
-^\[main\.pB\] always main.B == 11: PROVED$
+^\[main\.pA\] always main.A == 1: PROVED .*$
+^\[main\.pB\] always main.B == 11: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/bit-extract3.desc

@@ -3,10 +3,10 @@ bit-extract3.sv
 --module main
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.property1\] .*: PROVED$
-^\[main\.property2\] .*: PROVED$
-^\[main\.property3\] .*: PROVED$
-^\[main\.property4\] .*: PROVED$
-^\[main\.property5\] .*: PROVED$
+^\[main\.property1\] .*: PROVED .*$
+^\[main\.property2\] .*: PROVED .*$
+^\[main\.property3\] .*: PROVED .*$
+^\[main\.property4\] .*: PROVED .*$
+^\[main\.property5\] .*: PROVED .*$
 --
 ^warning: ignoring

regression/verilog/expressions/bit-extract5.desc

@@ -1,10 +1,10 @@
 CORE
 bit-extract5.sv
 --module main
-^\[main\.p0\] always main\.w1\[0\] && !main\.w1\[31\]: PROVED$
-^\[main\.p1\] always main\.w2\[0\] && !main\.w2\[31\]: PROVED$
-^\[main\.p2\] always main\.w3\[0\] && !main\.w3\[31\]: PROVED$
-^\[main\.p3\] always main\.w4\[0\] && !main\.w4\[31\]: PROVED$
+^\[main\.p0\] always main\.w1\[0\] && !main\.w1\[31\]: PROVED .*$
+^\[main\.p1\] always main\.w2\[0\] && !main\.w2\[31\]: PROVED .*$
+^\[main\.p2\] always main\.w3\[0\] && !main\.w3\[31\]: PROVED .*$
+^\[main\.p3\] always main\.w4\[0\] && !main\.w4\[31\]: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/bit-extract6.desc

@@ -1,8 +1,8 @@
 CORE
 bit-extract6.sv
 --module main
-^\[main\.p0\] always main\.index == 8 -> main\.vector\[7 - main\.index - 1\] == 1: PROVED$
-^\[main\.p1\] always main\.index >= 1 \&\& main\.index <= 7 -> main\.vector\[7 - main\.index - 1\] == 0: PROVED$
+^\[main\.p0\] always main\.index == 8 -> main\.vector\[7 - main\.index - 1\] == 1: PROVED .*$
+^\[main\.p1\] always main\.index >= 1 \&\& main\.index <= 7 -> main\.vector\[7 - main\.index - 1\] == 0: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --