EBMC: show proof engine in result

When using the engine selection heuristic, this adds the proof engine that
delivered the "PROVED" result to the result output.

Author: kroening

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/xnor1.desc

@@ -1,7 +1,7 @@
 CORE
 xnor1.smv
 
-^\[spec1\] G x: PROVED$
+^\[spec1\] G x: 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/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$
 --

regression/verilog/expressions/concatenation2.desc

@@ -3,7 +3,7 @@ concatenation2.v
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.property\.pA\] always main\.A == -1: PROVED$
-^\[main\.property\.pB\] always main\.B == 15: PROVED$
+^\[main\.property\.pA\] always main\.A == -1: PROVED .*$
+^\[main\.property\.pB\] always main\.B == 15: PROVED .*$
 --
 ^warning: ignoring

regression/verilog/expressions/concatenation3.desc

@@ -3,6 +3,6 @@ concatenation3.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\[.*\] always \{ 5'bxz01\?, 4'b10zx \} === 9'bxz01\?10zx: PROVED$
+^\[.*\] always \{ 5'bxz01\?, 4'b10zx \} === 9'bxz01\?10zx: PROVED .*$
 --
 ^warning: ignoring

regression/verilog/expressions/concatenation6.desc

@@ -1,7 +1,7 @@
 CORE
 concatenation6.sv
 
-^\[.*\] always main\.x == \{ 0, 1 \}: PROVED$
+^\[.*\] always main\.x == \{ 0, 1 \}: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/equality1.desc

@@ -1,18 +1,18 @@
 CORE broken-smt-backend
 equality1.v
 
-^\[.*\] always 10 == 10 === 1: PROVED$
-^\[.*\] always 10 == 20 === 0: PROVED$
-^\[.*\] always 10 != 20 === 1: PROVED$
-^\[.*\] always 10 == 20 === 0: PROVED$
-^\[.*\] always 32'b0000000000000000000000000000000x == 10 === 32'b0000000000000000000000000000000x: PROVED$
-^\[.*\] always 32'b0000000000000000000000000000000z == 20 === 32'b0000000000000000000000000000000x: PROVED$
-^\[.*\] always 32'b0000000000000000000000000000000x != 10 === 32'b0000000000000000000000000000000x: PROVED$
-^\[.*\] always 32'b0000000000000000000000000000000z != 20 === 32'b0000000000000000000000000000000x: PROVED$
-^\[.*\] always 1'sb1 == 2'b11 === 0: PROVED$
-^\[.*\] always 2'sb11 == 2'sb11 === 1: PROVED$
-^\[.*\] always 1\.1 == 1\.1 == 1: PROVED$
-^\[.*\] always 1\.1 == 1 == 0: PROVED$
+^\[.*\] always 10 == 10 === 1: PROVED .*$
+^\[.*\] always 10 == 20 === 0: PROVED .*$
+^\[.*\] always 10 != 20 === 1: PROVED .*$
+^\[.*\] always 10 == 20 === 0: PROVED .*$
+^\[.*\] always 32'b0000000000000000000000000000000x == 10 === 32'b0000000000000000000000000000000x: PROVED .*$
+^\[.*\] always 32'b0000000000000000000000000000000z == 20 === 32'b0000000000000000000000000000000x: PROVED .*$
+^\[.*\] always 32'b0000000000000000000000000000000x != 10 === 32'b0000000000000000000000000000000x: PROVED .*$
+^\[.*\] always 32'b0000000000000000000000000000000z != 20 === 32'b0000000000000000000000000000000x: PROVED .*$
+^\[.*\] always 1'sb1 == 2'b11 === 0: PROVED .*$
+^\[.*\] always 2'sb11 == 2'sb11 === 1: PROVED .*$
+^\[.*\] always 1\.1 == 1\.1 == 1: PROVED .*$
+^\[.*\] always 1\.1 == 1 == 0: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/equality2.desc

@@ -1,18 +1,18 @@
 CORE
 equality2.v
 
-^\[.*\] always 10 === 10 == 1: PROVED$
-^\[.*\] always 10 === 20 == 0: PROVED$
-^\[.*\] always 10 !== 10 == 0: PROVED$
-^\[.*\] always 10 !== 20 == 1: PROVED$
-^\[.*\] always 32'b0000000000000000000000000000000x === 32'b0000000000000000000000000000000x == 1: PROVED$
-^\[.*\] always 32'b0000000000000000000000000000000z === 32'b0000000000000000000000000000000z == 1: PROVED$
-^\[.*\] always 32'b0000000000000000000000000000000x === 32'b0000000000000000000000000000000z == 0: PROVED$
-^\[.*\] always 32'b0000000000000000000000000000000x === 1 == 0: PROVED$
-^\[.*\] always 32'b0000000000000000000000000000000z === 1 == 0: PROVED$
-^\[.*\] always 1 === 1 == 1: PROVED$
-^\[.*\] always 3'b011 === 2'sb11 == 1: PROVED$
-^\[.*\] always 3'sb111 === 3'sb111 == 1: PROVED$
+^\[.*\] always 10 === 10 == 1: PROVED .*$
+^\[.*\] always 10 === 20 == 0: PROVED .*$
+^\[.*\] always 10 !== 10 == 0: PROVED .*$
+^\[.*\] always 10 !== 20 == 1: PROVED .*$
+^\[.*\] always 32'b0000000000000000000000000000000x === 32'b0000000000000000000000000000000x == 1: PROVED .*$
+^\[.*\] always 32'b0000000000000000000000000000000z === 32'b0000000000000000000000000000000z == 1: PROVED .*$
+^\[.*\] always 32'b0000000000000000000000000000000x === 32'b0000000000000000000000000000000z == 0: PROVED .*$
+^\[.*\] always 32'b0000000000000000000000000000000x === 1 == 0: PROVED .*$
+^\[.*\] always 32'b0000000000000000000000000000000z === 1 == 0: PROVED .*$
+^\[.*\] always 1 === 1 == 1: PROVED .*$
+^\[.*\] always 3'b011 === 2'sb11 == 1: PROVED .*$
+^\[.*\] always 3'sb111 === 3'sb111 == 1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/inside1.desc

@@ -1,12 +1,12 @@
 CORE broken-smt-backend
 inside1.sv
 
-^\[.*\] always 2 inside \{1, 2, 3\}: PROVED$
-^\[.*\] always 2 inside \{3'b0\?0\}: PROVED$
-^\[.*\] always !\(2 inside \{3'b0\?1\}\): PROVED$
-^\[.*\] always 2 inside \{\[1:3\], \[6:8\]\}: PROVED$
-^\[.*\] always !\(4 inside \{\[1:3\], \[6:8\]\}\): PROVED$
-^\[.*\] always \(1 && 1\) inside \{1, 2, 3\}: PROVED$
+^\[.*\] always 2 inside \{1, 2, 3\}: PROVED .*$
+^\[.*\] always 2 inside \{3'b0\?0\}: PROVED .*$
+^\[.*\] always !\(2 inside \{3'b0\?1\}\): PROVED .*$
+^\[.*\] always 2 inside \{\[1:3\], \[6:8\]\}: PROVED .*$
+^\[.*\] always !\(4 inside \{\[1:3\], \[6:8\]\}\): PROVED .*$
+^\[.*\] always \(1 && 1\) inside \{1, 2, 3\}: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/part-select-constant1.desc

@@ -1,7 +1,7 @@
 CORE
 part-select-constant1.sv
 
-^\[.*\] .* PROVED$
+^\[.*\] .* PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/signed1.desc

@@ -1,14 +1,14 @@
 CORE
 signed1.sv
 --module main
-^\[main\.p1\] always main\.wire1 == main.wire2: PROVED$
-^\[main\.p2\] always main\.wire1 >>> 1 == -1: PROVED$
-^\[main\.p3\] always main\.wire2 >> 1 != -1: PROVED$
-^\[main\.p4\] always main\.wire1\[31:0\] >> 1 != -1: PROVED$
-^\[main\.p5\] always \$unsigned\(main\.wire1\) >> 1 != -1: PROVED$
-^\[main\.p6\] always \$signed\(main\.wire2\) >>> 1 == -1: PROVED$
-^\[main\.p7\] always -1 >> 1 != -1: PROVED$
-^\[main\.p8\] always -1 >>> 1 == -1: PROVED$
+^\[main\.p1\] always main\.wire1 == main.wire2: PROVED .*$
+^\[main\.p2\] always main\.wire1 >>> 1 == -1: PROVED .*$
+^\[main\.p3\] always main\.wire2 >> 1 != -1: PROVED .*$
+^\[main\.p4\] always main\.wire1\[31:0\] >> 1 != -1: PROVED .*$
+^\[main\.p5\] always \$unsigned\(main\.wire1\) >> 1 != -1: PROVED .*$
+^\[main\.p6\] always \$signed\(main\.wire2\) >>> 1 == -1: PROVED .*$
+^\[main\.p7\] always -1 >> 1 != -1: PROVED .*$
+^\[main\.p8\] always -1 >>> 1 == -1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/signing_cast1.desc

@@ -1,12 +1,12 @@
 CORE broken-smt-backend
 signing_cast1.sv
 --module main
-^\[main\.p0\] always signed'\(1'b1\) == -1: PROVED$
-^\[main\.p1\] always signed'\(4'b1110\) == -2: PROVED$
-^\[main\.p2\] always signed'\(4'b0111\) == 7: PROVED$
-^\[main\.p3\] always signed'\(!0\) == -1: PROVED$
-^\[main\.p4\] always unsigned'\(!0\) == 1: PROVED$
-^\[main\.p5\] always unsigned'\(-1\) == 32'hFFFFFFFF: PROVED$
+^\[main\.p0\] always signed'\(1'b1\) == -1: PROVED .*$
+^\[main\.p1\] always signed'\(4'b1110\) == -2: PROVED .*$
+^\[main\.p2\] always signed'\(4'b0111\) == 7: PROVED .*$
+^\[main\.p3\] always signed'\(!0\) == -1: PROVED .*$
+^\[main\.p4\] always unsigned'\(!0\) == 1: PROVED .*$
+^\[main\.p5\] always unsigned'\(-1\) == 32'hFFFFFFFF: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --