diff --git a/regression/ebmc/engine-heuristic/basic2.desc b/regression/ebmc/engine-heuristic/basic2.desc
index e8adb78c1..b59ddcfbb 100644
--- a/regression/ebmc/engine-heuristic/basic2.desc
+++ b/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$
 --
diff --git a/regression/ebmc/example1/test.desc b/regression/ebmc/example1/test.desc
index b7d5f7b13..38f4c2ab7 100644
--- a/regression/ebmc/example1/test.desc
+++ b/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$
diff --git a/regression/smv/enums/enum1.desc b/regression/smv/enums/enum1.desc
index f1059302c..a81189dd2 100644
--- a/regression/smv/enums/enum1.desc
+++ b/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$
 --
diff --git a/regression/smv/expressions/smv_if2.desc b/regression/smv/expressions/smv_if2.desc
index 50915489d..e001c9d36 100644
--- a/regression/smv/expressions/smv_if2.desc
+++ b/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$
 --
diff --git a/regression/smv/expressions/xnor1.desc b/regression/smv/expressions/xnor1.desc
index d535ab04e..0d7d8487e 100644
--- a/regression/smv/expressions/xnor1.desc
+++ b/regression/smv/expressions/xnor1.desc
@@ -1,7 +1,7 @@
 CORE
 xnor1.smv
 
-^\[spec1\] G x: PROVED$
+^\[spec1\] G x: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/smv/smv/initial1.desc b/regression/smv/smv/initial1.desc
index 3b6e01d0c..fda50389f 100644
--- a/regression/smv/smv/initial1.desc
+++ b/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$
diff --git a/regression/smv/word/bitwise1.desc b/regression/smv/word/bitwise1.desc
index faf6762a0..618cca9ff 100644
--- a/regression/smv/word/bitwise1.desc
+++ b/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$
 --
diff --git a/regression/smv/word/concat1.desc b/regression/smv/word/concat1.desc
index d1326406b..4cd9ae484 100644
--- a/regression/smv/word/concat1.desc
+++ b/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$
 --
diff --git a/regression/smv/word/extend1.desc b/regression/smv/word/extend1.desc
index 949ec0eed..fc5cb49d0 100644
--- a/regression/smv/word/extend1.desc
+++ b/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$
 --
diff --git a/regression/smv/word/resize1.desc b/regression/smv/word/resize1.desc
index 3ba90bc13..ddc0625ee 100644
--- a/regression/smv/word/resize1.desc
+++ b/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$
 --
diff --git a/regression/smv/word/shift1.desc b/regression/smv/word/shift1.desc
index 60c54ff8d..09663b344 100644
--- a/regression/smv/word/shift1.desc
+++ b/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$
 --
diff --git a/regression/smv/word/signed1.desc b/regression/smv/word/signed1.desc
index 9381a6469..5175f6b61 100644
--- a/regression/smv/word/signed1.desc
+++ b/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$
 --
diff --git a/regression/smv/word/unsigned1.desc b/regression/smv/word/unsigned1.desc
index 6f85f6d80..dc94076d2 100644
--- a/regression/smv/word/unsigned1.desc
+++ b/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$
 --
diff --git a/regression/verilog/SVA/immediate2.desc b/regression/verilog/SVA/immediate2.desc
index 0c429e7b3..8304a8662 100644
--- a/regression/verilog/SVA/immediate2.desc
+++ b/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$
diff --git a/regression/verilog/SVA/immediate3.desc b/regression/verilog/SVA/immediate3.desc
index 1179a40a5..62db6b782 100644
--- a/regression/verilog/SVA/immediate3.desc
+++ b/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$
 --
diff --git a/regression/verilog/SVA/initial1.bmc.desc b/regression/verilog/SVA/initial1.bmc.desc
index 63335e32b..629cdf92f 100644
--- a/regression/verilog/SVA/initial1.bmc.desc
+++ b/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$
 --
diff --git a/regression/verilog/SVA/initial2.desc b/regression/verilog/SVA/initial2.desc
index 1f3fc24d4..22b6a1662 100644
--- a/regression/verilog/SVA/initial2.desc
+++ b/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$
 --
diff --git a/regression/verilog/SVA/sequence5.desc b/regression/verilog/SVA/sequence5.desc
index 825b672e0..b3cb3a6a2 100644
--- a/regression/verilog/SVA/sequence5.desc
+++ b/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$
diff --git a/regression/verilog/SVA/sequence_or1.bmc.desc b/regression/verilog/SVA/sequence_or1.bmc.desc
index d029c5f7a..c2800b602 100644
--- a/regression/verilog/SVA/sequence_or1.bmc.desc
+++ b/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+$
diff --git a/regression/verilog/SVA/static_final1.desc b/regression/verilog/SVA/static_final1.desc
index 768df3e2e..e2ced9180 100644
--- a/regression/verilog/SVA/static_final1.desc
+++ b/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$
 --
diff --git a/regression/verilog/SVA/sva_and1.desc b/regression/verilog/SVA/sva_and1.desc
index 2facd225b..e118132b0 100644
--- a/regression/verilog/SVA/sva_and1.desc
+++ b/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$
diff --git a/regression/verilog/SVA/sva_iff1.desc b/regression/verilog/SVA/sva_iff1.desc
index ed75e00d7..3582a9bb4 100644
--- a/regression/verilog/SVA/sva_iff1.desc
+++ b/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$
diff --git a/regression/verilog/SVA/sva_implies1.desc b/regression/verilog/SVA/sva_implies1.desc
index 53284a212..182ce4a6b 100644
--- a/regression/verilog/SVA/sva_implies1.desc
+++ b/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$
diff --git a/regression/verilog/case/nested_case1.desc b/regression/verilog/case/nested_case1.desc
index 9a38264e2..4739b6902 100644
--- a/regression/verilog/case/nested_case1.desc
+++ b/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
diff --git a/regression/verilog/case/riscv-alu.desc b/regression/verilog/case/riscv-alu.desc
index b88afd892..592468865 100644
--- a/regression/verilog/case/riscv-alu.desc
+++ b/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$
 --
diff --git a/regression/verilog/data-types/chandle1.desc b/regression/verilog/data-types/chandle1.desc
index a840983e1..12cf2249b 100644
--- a/regression/verilog/data-types/chandle1.desc
+++ b/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$
 --
diff --git a/regression/verilog/data-types/vector_types2.desc b/regression/verilog/data-types/vector_types2.desc
index acaf22221..a789cc0d2 100644
--- a/regression/verilog/data-types/vector_types2.desc
+++ b/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$
 --
diff --git a/regression/verilog/enums/enum4.desc b/regression/verilog/enums/enum4.desc
index febeea473..4e719ce42 100644
--- a/regression/verilog/enums/enum4.desc
+++ b/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 .*$
 --
diff --git a/regression/verilog/enums/enum_base_type1.desc b/regression/verilog/enums/enum_base_type1.desc
index a766c9db6..33f74ef1a 100644
--- a/regression/verilog/enums/enum_base_type1.desc
+++ b/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 .*$
 --
diff --git a/regression/verilog/enums/enum_base_type2.desc b/regression/verilog/enums/enum_base_type2.desc
index 8f0c073eb..8959d7bb9 100644
--- a/regression/verilog/enums/enum_base_type2.desc
+++ b/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 .*$
 --
diff --git a/regression/verilog/enums/enum_cast1.desc b/regression/verilog/enums/enum_cast1.desc
index 2880369f7..ecf4132f8 100644
--- a/regression/verilog/enums/enum_cast1.desc
+++ b/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 .*$
 --
diff --git a/regression/verilog/enums/enum_initializers1.desc b/regression/verilog/enums/enum_initializers1.desc
index c3bc0081d..b4a8472f6 100644
--- a/regression/verilog/enums/enum_initializers1.desc
+++ b/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$
 --
diff --git a/regression/verilog/expressions/bit-extract3.desc b/regression/verilog/expressions/bit-extract3.desc
index 408addae2..9f34e9c2a 100644
--- a/regression/verilog/expressions/bit-extract3.desc
+++ b/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
diff --git a/regression/verilog/expressions/bit-extract5.desc b/regression/verilog/expressions/bit-extract5.desc
index 1c1fb0a92..094ad5cb7 100644
--- a/regression/verilog/expressions/bit-extract5.desc
+++ b/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$
 --
diff --git a/regression/verilog/expressions/bit-extract6.desc b/regression/verilog/expressions/bit-extract6.desc
index 3f83ddb7f..17f9f1cb3 100644
--- a/regression/verilog/expressions/bit-extract6.desc
+++ b/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$
 --
diff --git a/regression/verilog/expressions/concatenation2.desc b/regression/verilog/expressions/concatenation2.desc
index b3365b081..5702b5fd4 100644
--- a/regression/verilog/expressions/concatenation2.desc
+++ b/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
diff --git a/regression/verilog/expressions/concatenation3.desc b/regression/verilog/expressions/concatenation3.desc
index 6dde1e1c3..0de8342e8 100644
--- a/regression/verilog/expressions/concatenation3.desc
+++ b/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
diff --git a/regression/verilog/expressions/concatenation6.desc b/regression/verilog/expressions/concatenation6.desc
index 22845f9f7..facf5389e 100644
--- a/regression/verilog/expressions/concatenation6.desc
+++ b/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$
 --
diff --git a/regression/verilog/expressions/equality1.desc b/regression/verilog/expressions/equality1.desc
index ae31d7857..e9fed273e 100644
--- a/regression/verilog/expressions/equality1.desc
+++ b/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$
 --
diff --git a/regression/verilog/expressions/equality2.desc b/regression/verilog/expressions/equality2.desc
index 06b945da5..f70993dbe 100644
--- a/regression/verilog/expressions/equality2.desc
+++ b/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$
 --
diff --git a/regression/verilog/expressions/inside1.desc b/regression/verilog/expressions/inside1.desc
index 2fcb31e5a..2b4f9eb87 100644
--- a/regression/verilog/expressions/inside1.desc
+++ b/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$
 --
diff --git a/regression/verilog/expressions/part-select-constant1.desc b/regression/verilog/expressions/part-select-constant1.desc
index 1508484de..a5f752246 100644
--- a/regression/verilog/expressions/part-select-constant1.desc
+++ b/regression/verilog/expressions/part-select-constant1.desc
@@ -1,7 +1,7 @@
 CORE
 part-select-constant1.sv
 
-^\[.*\] .* PROVED$
+^\[.*\] .* PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/expressions/signed1.desc b/regression/verilog/expressions/signed1.desc
index 119daeba5..b766fc7b0 100644
--- a/regression/verilog/expressions/signed1.desc
+++ b/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$
 --
diff --git a/regression/verilog/expressions/signing_cast1.desc b/regression/verilog/expressions/signing_cast1.desc
index b8731bb59..619d6bb2b 100644
--- a/regression/verilog/expressions/signing_cast1.desc
+++ b/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$
 --
diff --git a/regression/verilog/expressions/size_cast1.desc b/regression/verilog/expressions/size_cast1.desc
index 8afe24233..3ea795cfa 100644
--- a/regression/verilog/expressions/size_cast1.desc
+++ b/regression/verilog/expressions/size_cast1.desc
@@ -1,10 +1,10 @@
 CORE
 size_cast1.sv
 --module main
-^\[main\.p0\] always \$bits\(10'\(1\)\) == 10: PROVED$
-^\[main\.p1\] always \$bits\(20'\(1\)\) == 20: PROVED$
-^\[main\.p2\] always 10'\(-1\) == -1: PROVED$
-^\[main\.p3\] always 2'\(1 == 1\) == 1: PROVED$
+^\[main\.p0\] always \$bits\(10'\(1\)\) == 10: PROVED .*$
+^\[main\.p1\] always \$bits\(20'\(1\)\) == 20: PROVED .*$
+^\[main\.p2\] always 10'\(-1\) == -1: PROVED .*$
+^\[main\.p3\] always 2'\(1 == 1\) == 1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/expressions/static_cast1.desc b/regression/verilog/expressions/static_cast1.desc
index 838ec3718..c51e3ed42 100644
--- a/regression/verilog/expressions/static_cast1.desc
+++ b/regression/verilog/expressions/static_cast1.desc
@@ -1,7 +1,7 @@
 CORE
 static_cast1.sv
 --module main
-^\[main\.p0\] always \[7:0\]'\(32'hFFFF\) == 255: PROVED$
+^\[main\.p0\] always \[7:0\]'\(32'hFFFF\) == 255: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/expressions/streaming_concatenation1.desc b/regression/verilog/expressions/streaming_concatenation1.desc
index 6b0d09766..91af1f22f 100644
--- a/regression/verilog/expressions/streaming_concatenation1.desc
+++ b/regression/verilog/expressions/streaming_concatenation1.desc
@@ -1,10 +1,10 @@
 CORE
 streaming_concatenation1.sv
 
-^\[.*\] always \{<<\{4'b1010\}\} == 4'b0101: PROVED$
-^\[.*\] always \{<<\{1 == 1\}\} == 1: PROVED$
-^\[.*\] always \{<<4\{16'hABCD\}\} == 16'hDCBA: PROVED$
-^\[.*\] always \{<<8\{16'hABCD\}\} == 16'hCDAB: PROVED$
+^\[.*\] always \{<<\{4'b1010\}\} == 4'b0101: PROVED .*$
+^\[.*\] always \{<<\{1 == 1\}\} == 1: PROVED .*$
+^\[.*\] always \{<<4\{16'hABCD\}\} == 16'hDCBA: PROVED .*$
+^\[.*\] always \{<<8\{16'hABCD\}\} == 16'hCDAB: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/expressions/wildcard_equality1.desc b/regression/verilog/expressions/wildcard_equality1.desc
index c7efea341..6d9359abc 100644
--- a/regression/verilog/expressions/wildcard_equality1.desc
+++ b/regression/verilog/expressions/wildcard_equality1.desc
@@ -1,16 +1,16 @@
 CORE
 wildcard_equality1.sv
 
-^\[main\.property01\] always 10 ==\? 10 === 1: PROVED$
-^\[main\.property02\] always 10 ==\? 20 === 0: PROVED$
-^\[main\.property03\] always 10 !=\? 20 === 1: PROVED$
-^\[main\.property04\] always 10 ==\? 20 === 0: PROVED$
-^\[main\.property05\] always 2'b00 ==\? 2'b0x === 1: PROVED$
-^\[main\.property06\] always 2'b10 ==\? 2'b0x === 0: PROVED$
-^\[main\.property07\] always 2'b00 !=\? 2'b0x === 0: PROVED$
-^\[main\.property08\] always 2'b10 !=\? 2'b0x === 1: PROVED$
+^\[main\.property01\] always 10 ==\? 10 === 1: PROVED .*$
+^\[main\.property02\] always 10 ==\? 20 === 0: PROVED .*$
+^\[main\.property03\] always 10 !=\? 20 === 1: PROVED .*$
+^\[main\.property04\] always 10 ==\? 20 === 0: PROVED .*$
+^\[main\.property05\] always 2'b00 ==\? 2'b0x === 1: PROVED .*$
+^\[main\.property06\] always 2'b10 ==\? 2'b0x === 0: PROVED .*$
+^\[main\.property07\] always 2'b00 !=\? 2'b0x === 0: PROVED .*$
+^\[main\.property08\] always 2'b10 !=\? 2'b0x === 1: PROVED .*$
 ^\[main\.property09\] always 2'b11 ==\? 2'b11 === 0: REFUTED$
-^\[main\.property10\] always 2'sb11 ==\? 2'sb11 === 1: PROVED$
+^\[main\.property10\] always 2'sb11 ==\? 2'sb11 === 1: PROVED .*$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/functioncall/function_ports1.desc b/regression/verilog/functioncall/function_ports1.desc
index f4c3bc1c7..557ac569e 100644
--- a/regression/verilog/functioncall/function_ports1.desc
+++ b/regression/verilog/functioncall/function_ports1.desc
@@ -3,6 +3,6 @@ function_ports1.v
 --module main
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.property\.test16\] always .*: PROVED$
+^\[main\.property\.test16\] always .*: PROVED .*$
 --
 ^warning: ignoring
diff --git a/regression/verilog/functioncall/functioncall1.desc b/regression/verilog/functioncall/functioncall1.desc
index deb64858d..f70a28aac 100644
--- a/regression/verilog/functioncall/functioncall1.desc
+++ b/regression/verilog/functioncall/functioncall1.desc
@@ -3,6 +3,6 @@ functioncall1.v
 --module main
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.property\.test1\] always .*: PROVED$
+^\[main\.property\.test1\] always .*: PROVED .*$
 --
 ^warning: ignoring
diff --git a/regression/verilog/functioncall/functioncall6.desc b/regression/verilog/functioncall/functioncall6.desc
index eb0326034..4fad8f8dd 100644
--- a/regression/verilog/functioncall/functioncall6.desc
+++ b/regression/verilog/functioncall/functioncall6.desc
@@ -3,6 +3,6 @@ functioncall6.v
 --module main
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.property\.p1\] always .*: PROVED$
+^\[main\.property\.p1\] always .*: PROVED .*$
 --
 ^warning: ignoring
diff --git a/regression/verilog/modules/type_parameters1.desc b/regression/verilog/modules/type_parameters1.desc
index 361671b40..c68a2b87d 100644
--- a/regression/verilog/modules/type_parameters1.desc
+++ b/regression/verilog/modules/type_parameters1.desc
@@ -1,8 +1,8 @@
 CORE
 type_parameters1.sv
 
-^\[main\.p1\] always \$bits\(main\.T1\) == 1: PROVED$
-^\[main\.p2\] always \$bits\(main\.T2\) == 32: PROVED$
+^\[main\.p1\] always \$bits\(main\.T1\) == 1: PROVED .*$
+^\[main\.p2\] always \$bits\(main\.T2\) == 32: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/packages/package2.desc b/regression/verilog/packages/package2.desc
index e2d2ae358..6d7a2e794 100644
--- a/regression/verilog/packages/package2.desc
+++ b/regression/verilog/packages/package2.desc
@@ -1,7 +1,7 @@
 CORE
 package2.sv
 
-^^\[.*\] always main\.Q == 123: PROVED$
+^^\[.*\] always main\.Q == 123: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/primitive_gates/nand2.desc b/regression/verilog/primitive_gates/nand2.desc
index d11be3eaa..46a6fee42 100644
--- a/regression/verilog/primitive_gates/nand2.desc
+++ b/regression/verilog/primitive_gates/nand2.desc
@@ -1,8 +1,8 @@
 CORE broken-smt-backend
 nand2.sv
 
-^\[main\.nand_ok\] always !main\.nand_in1 == main\.nand_out: PROVED$
-^\[main\.nand_is_reduction_nand\] always ~\&\{ main\.nand_in1 \} == main\.nand_out: PROVED$
+^\[main\.nand_ok\] always !main\.nand_in1 == main\.nand_out: PROVED .*$
+^\[main\.nand_is_reduction_nand\] always ~\&\{ main\.nand_in1 \} == main\.nand_out: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/primitive_gates/nor2.desc b/regression/verilog/primitive_gates/nor2.desc
index 8a51a6c05..9449289e6 100644
--- a/regression/verilog/primitive_gates/nor2.desc
+++ b/regression/verilog/primitive_gates/nor2.desc
@@ -1,8 +1,8 @@
 CORE broken-smt-backend
 nor2.sv
 
-^\[main\.nor_ok\] always !main\.nor_in1 == main\.nor_out: PROVED$
-^\[main\.nor_is_reduction_nor\] always ~\|\{ main\.nor_in1 \} == main\.nor_out: PROVED$
+^\[main\.nor_ok\] always !main\.nor_in1 == main\.nor_out: PROVED .*$
+^\[main\.nor_is_reduction_nor\] always ~\|\{ main\.nor_in1 \} == main\.nor_out: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/primitive_gates/xnor1.desc b/regression/verilog/primitive_gates/xnor1.desc
index 092ab8f26..e4128c4ee 100644
--- a/regression/verilog/primitive_gates/xnor1.desc
+++ b/regression/verilog/primitive_gates/xnor1.desc
@@ -1,9 +1,9 @@
 CORE broken-smt-backend
 xnor1.sv
 
-^\[main\.xnor_ok\] always !xor\(xor\(main\.xnor_in1, main\.xnor_in2\), main\.xnor_in3\) == main\.xnor_out: PROVED$
+^\[main\.xnor_ok\] always !xor\(xor\(main\.xnor_in1, main\.xnor_in2\), main\.xnor_in3\) == main\.xnor_out: PROVED .*$
 ^\[main\.xnor_fail\] always main\.xnor_in1 == main\.xnor_in2 == main\.xnor_in3 == main\.xnor_out: REFUTED$
-^\[main\.xnor_is_reduction_xnor\] always ~\^\{ main\.xnor_in1, main\.xnor_in2, main\.xnor_in3 \} == main\.xnor_out: PROVED$
+^\[main\.xnor_is_reduction_xnor\] always ~\^\{ main\.xnor_in1, main\.xnor_in2, main\.xnor_in3 \} == main\.xnor_out: PROVED .*$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/primitive_gates/xnor2.desc b/regression/verilog/primitive_gates/xnor2.desc
index cd90f0c8a..ce5a2d3c3 100644
--- a/regression/verilog/primitive_gates/xnor2.desc
+++ b/regression/verilog/primitive_gates/xnor2.desc
@@ -1,8 +1,8 @@
 CORE broken-smt-backend
 xnor2.sv
 
-^\[main\.xnor_ok\] always !main\.xnor_in1 == main\.xnor_out: PROVED$
-^\[main\.xnor_is_reduction_xnor\] always ~\^\{ main\.xnor_in1 \} == main\.xnor_out: PROVED$
+^\[main\.xnor_ok\] always !main\.xnor_in1 == main\.xnor_out: PROVED .*$
+^\[main\.xnor_is_reduction_xnor\] always ~\^\{ main\.xnor_in1 \} == main\.xnor_out: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/primitive_gates/xnor3.desc b/regression/verilog/primitive_gates/xnor3.desc
index 465a26c4a..3c76be8e9 100644
--- a/regression/verilog/primitive_gates/xnor3.desc
+++ b/regression/verilog/primitive_gates/xnor3.desc
@@ -1,7 +1,7 @@
 CORE
 xnor3.sv
 
-^\[main\.xnor_ok\] always main\.xnor_in1 ~\^ main\.xnor_in2 == main\.xnor_out: PROVED$
+^\[main\.xnor_ok\] always main\.xnor_in1 ~\^ main\.xnor_in2 == main\.xnor_out: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/primitive_gates/xnor4.desc b/regression/verilog/primitive_gates/xnor4.desc
index 5020f9ded..50ac07323 100644
--- a/regression/verilog/primitive_gates/xnor4.desc
+++ b/regression/verilog/primitive_gates/xnor4.desc
@@ -1,8 +1,8 @@
 CORE broken-smt-backend
 xnor4.sv
 
-^\[main\.xnor_x1_ok\] always ~\(main\.xnor_in1 \^ main\.xnor_in2 \^ main.xnor_in3\) == main.xnor_out: PROVED$
-^\[main\.xnor_x2_ok\] always ~main\.xnor_in1 == main.xnor_out: PROVED$
+^\[main\.xnor_x1_ok\] always ~\(main\.xnor_in1 \^ main\.xnor_in2 \^ main.xnor_in3\) == main.xnor_out: PROVED .*$
+^\[main\.xnor_x2_ok\] always ~main\.xnor_in1 == main.xnor_out: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/property/named_property1.desc b/regression/verilog/property/named_property1.desc
index 5577d0b89..b325e7567 100644
--- a/regression/verilog/property/named_property1.desc
+++ b/regression/verilog/property/named_property1.desc
@@ -1,7 +1,7 @@
 CORE
 named_property1.sv
 
-^\[main\.assert\.1\] always main\.x_is_ten: PROVED$
+^\[main\.assert\.1\] always main\.x_is_ten: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/structs/structs1.desc b/regression/verilog/structs/structs1.desc
index 8a017cb59..380b043a4 100644
--- a/regression/verilog/structs/structs1.desc
+++ b/regression/verilog/structs/structs1.desc
@@ -1,10 +1,10 @@
 CORE
 structs1.sv
 
-^\[main\.p0\] always \$bits\(main\.s\) == 9: PROVED$
-^\[main\.p1\] always main\.s\.field1 == 1: PROVED$
-^\[main\.p2\] always main\.s\.field2 == 0: PROVED$
-^\[main\.p3\] always main\.s\.field3 == 115: PROVED$
+^\[main\.p0\] always \$bits\(main\.s\) == 9: PROVED .*$
+^\[main\.p1\] always main\.s\.field1 == 1: PROVED .*$
+^\[main\.p2\] always main\.s\.field2 == 0: PROVED .*$
+^\[main\.p3\] always main\.s\.field3 == 115: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/structs/structs4.desc b/regression/verilog/structs/structs4.desc
index 83b3684c6..388e79130 100644
--- a/regression/verilog/structs/structs4.desc
+++ b/regression/verilog/structs/structs4.desc
@@ -1,7 +1,7 @@
 CORE
 structs4.sv
 
-^\[main\.p0\] always main\.w == 32'h173: PROVED$
+^\[main\.p0\] always main\.w == 32'h173: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/structs/structs5.desc b/regression/verilog/structs/structs5.desc
index ae3ba0123..ef63677fa 100644
--- a/regression/verilog/structs/structs5.desc
+++ b/regression/verilog/structs/structs5.desc
@@ -1,9 +1,9 @@
 CORE
 structs5.sv
 
-^\[main\.p1\] always main\.s\.field1 == 1: PROVED$
-^\[main\.p2\] always main\.s\.field2 == 0: PROVED$
-^\[main\.p3\] always main\.s\.field3 == 115: PROVED$
+^\[main\.p1\] always main\.s\.field1 == 1: PROVED .*$
+^\[main\.p2\] always main\.s\.field2 == 0: PROVED .*$
+^\[main\.p3\] always main\.s\.field3 == 115: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/synthesis/always_comb2.desc b/regression/verilog/synthesis/always_comb2.desc
index 523cc7505..23b53c1aa 100644
--- a/regression/verilog/synthesis/always_comb2.desc
+++ b/regression/verilog/synthesis/always_comb2.desc
@@ -1,9 +1,9 @@
 CORE
 always_comb2.sv
 
-^\[main\.p0\] always main\.data == 0 -> main\.decoded == 1: PROVED$
-^\[main\.p1\] always main\.data == 1 -> main\.decoded == 2: PROVED$
-^\[main\.p2\] always main\.data == 2 -> main\.decoded == 4: PROVED$
+^\[main\.p0\] always main\.data == 0 -> main\.decoded == 1: PROVED .*$
+^\[main\.p1\] always main\.data == 1 -> main\.decoded == 2: PROVED .*$
+^\[main\.p2\] always main\.data == 2 -> main\.decoded == 4: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.desc b/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.desc
index 1541189bf..5c2706a87 100644
--- a/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.desc
+++ b/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.desc
@@ -1,7 +1,7 @@
 CORE
 continuous_assignment_to_variable_systemverilog.sv
 
-^\[main\.p1\] always main\.some_reg == main\.i: PROVED$
+^\[main\.p1\] always main\.some_reg == main\.i: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/system-functions/array_functions1.desc b/regression/verilog/system-functions/array_functions1.desc
index b3b7fe187..90be2e632 100644
--- a/regression/verilog/system-functions/array_functions1.desc
+++ b/regression/verilog/system-functions/array_functions1.desc
@@ -1,21 +1,21 @@
 CORE
 array_functions1.sv
 --module main
-^\[main\.pP0\] always \$left\(main\.packed1\) == 32 && \$right\(main\.packed1\) == 1: PROVED$
-^\[main\.pP1\] always \$left\(main\.packed2\) == 0 && \$right\(main\.packed2\) == 31: PROVED$
-^\[main\.pP2\] always \$low\(main\.packed1\) == 1 && \$high\(main\.packed1\) == 32: PROVED$
-^\[main\.pP3\] always \$low\(main\.packed2\) == 0 && \$high\(main\.packed2\) == 31: PROVED$
-^\[main\.pP4\] always \$increment\(main\.packed1\) == 1: PROVED$
-^\[main\.pP5\] always \$increment\(main\.packed2\) == -1: PROVED$
-^\[main\.pU0\] always \$left\(main\.unpacked1\) == 32 && \$right\(main\.unpacked1\) == 1: PROVED$
-^\[main\.pU1\] always \$left\(main\.unpacked2\) == 0 && \$right\(main\.unpacked2\) == 31: PROVED$
-^\[main\.pU2\] always \$left\(main\.unpacked3\) == 31 && \$right\(main\.unpacked3\) == 0: PROVED$
-^\[main\.pU3\] always \$low\(main\.unpacked1\) == 1 && \$high\(main\.unpacked1\) == 32: PROVED$
-^\[main\.pU4\] always \$low\(main\.unpacked2\) == 0 && \$high\(main\.unpacked2\) == 31: PROVED$
-^\[main\.pU5\] always \$low\(main\.unpacked3\) == 0 && \$high\(main\.unpacked3\) == 31: PROVED$
-^\[main\.pU6\] always \$increment\(main\.unpacked1\) == 1: PROVED$
-^\[main\.pU7\] always \$increment\(main\.unpacked2\) == -1: PROVED$
-^\[main\.pU8\] always \$increment\(main\.unpacked3\) == 1: PROVED$
+^\[main\.pP0\] always \$left\(main\.packed1\) == 32 && \$right\(main\.packed1\) == 1: PROVED .*$
+^\[main\.pP1\] always \$left\(main\.packed2\) == 0 && \$right\(main\.packed2\) == 31: PROVED .*$
+^\[main\.pP2\] always \$low\(main\.packed1\) == 1 && \$high\(main\.packed1\) == 32: PROVED .*$
+^\[main\.pP3\] always \$low\(main\.packed2\) == 0 && \$high\(main\.packed2\) == 31: PROVED .*$
+^\[main\.pP4\] always \$increment\(main\.packed1\) == 1: PROVED .*$
+^\[main\.pP5\] always \$increment\(main\.packed2\) == -1: PROVED .*$
+^\[main\.pU0\] always \$left\(main\.unpacked1\) == 32 && \$right\(main\.unpacked1\) == 1: PROVED .*$
+^\[main\.pU1\] always \$left\(main\.unpacked2\) == 0 && \$right\(main\.unpacked2\) == 31: PROVED .*$
+^\[main\.pU2\] always \$left\(main\.unpacked3\) == 31 && \$right\(main\.unpacked3\) == 0: PROVED .*$
+^\[main\.pU3\] always \$low\(main\.unpacked1\) == 1 && \$high\(main\.unpacked1\) == 32: PROVED .*$
+^\[main\.pU4\] always \$low\(main\.unpacked2\) == 0 && \$high\(main\.unpacked2\) == 31: PROVED .*$
+^\[main\.pU5\] always \$low\(main\.unpacked3\) == 0 && \$high\(main\.unpacked3\) == 31: PROVED .*$
+^\[main\.pU6\] always \$increment\(main\.unpacked1\) == 1: PROVED .*$
+^\[main\.pU7\] always \$increment\(main\.unpacked2\) == -1: PROVED .*$
+^\[main\.pU8\] always \$increment\(main\.unpacked3\) == 1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/system-functions/clog2.desc b/regression/verilog/system-functions/clog2.desc
index 5eda64e9c..8e9e78c80 100644
--- a/regression/verilog/system-functions/clog2.desc
+++ b/regression/verilog/system-functions/clog2.desc
@@ -3,12 +3,12 @@ clog2.v
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.property.p0\] .* PROVED$
-^\[main.property.p1\] .* PROVED$
-^\[main.property.p2\] .* PROVED$
-^\[main.property.p3\] .* PROVED$
-^\[main.property.p4\] .* PROVED$
-^\[main.property.p5\] .* PROVED$
-^\[main.property.p6\] .* PROVED$
+^\[main.property.p0\] .* PROVED .*$
+^\[main.property.p1\] .* PROVED .*$
+^\[main.property.p2\] .* PROVED .*$
+^\[main.property.p3\] .* PROVED .*$
+^\[main.property.p4\] .* PROVED .*$
+^\[main.property.p5\] .* PROVED .*$
+^\[main.property.p6\] .* PROVED .*$
 --
 ^warning: ignoring
diff --git a/regression/verilog/system-functions/signed2.desc b/regression/verilog/system-functions/signed2.desc
index db8b85fe0..eea5d40be 100644
--- a/regression/verilog/system-functions/signed2.desc
+++ b/regression/verilog/system-functions/signed2.desc
@@ -1,10 +1,10 @@
 CORE
 signed2.sv
 
-^\[main\.p0\] always \$signed\(1\) == 1: PROVED$
-^\[main\.p1\] always \$signed\(1'b1\) == -1: PROVED$
-^\[main\.p2\] always \$signed\(-1\) == -1: PROVED$
-^\[main\.p3\] always \$signed\(!0\) == -1: PROVED$
+^\[main\.p0\] always \$signed\(1\) == 1: PROVED .*$
+^\[main\.p1\] always \$signed\(1'b1\) == -1: PROVED .*$
+^\[main\.p2\] always \$signed\(-1\) == -1: PROVED .*$
+^\[main\.p3\] always \$signed\(!0\) == -1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/system-functions/typename1.desc b/regression/verilog/system-functions/typename1.desc
index db332884d..4c3bc5314 100644
--- a/regression/verilog/system-functions/typename1.desc
+++ b/regression/verilog/system-functions/typename1.desc
@@ -1,13 +1,13 @@
 CORE
 typename1.sv
 --module main
-^\[.*\] always \$typename\(main\.some_bit\) == "bit": PROVED$
-^\[.*\] always \$typename\(main\.vector1\) == "bit\[31:0\]": PROVED$
-^\[.*\] always \$typename\(main\.vector2\) == "bit\[0:31\]": PROVED$
-^\[.*\] always \$typename\(main\.vector3\) == "bit signed\[31:0\]": PROVED$
-^\[.*\] always \$typename\(real'\(1\)\) == "real": PROVED$
-^\[.*\] always \$typename\(shortreal'\(1\)\) == "shortreal": PROVED$
-^\[.*\] always \$typename\(realtime'\(1\)\) == "realtime": PROVED$
+^\[.*\] always \$typename\(main\.some_bit\) == "bit": PROVED .*$
+^\[.*\] always \$typename\(main\.vector1\) == "bit\[31:0\]": PROVED .*$
+^\[.*\] always \$typename\(main\.vector2\) == "bit\[0:31\]": PROVED .*$
+^\[.*\] always \$typename\(main\.vector3\) == "bit signed\[31:0\]": PROVED .*$
+^\[.*\] always \$typename\(real'\(1\)\) == "real": PROVED .*$
+^\[.*\] always \$typename\(shortreal'\(1\)\) == "shortreal": PROVED .*$
+^\[.*\] always \$typename\(realtime'\(1\)\) == "realtime": PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp
index 2fb032c40..84dce9e28 100644
--- a/src/ebmc/bdd_engine.cpp
+++ b/src/ebmc/bdd_engine.cpp
@@ -592,7 +592,7 @@ void bdd_enginet::check_AGp(propertyt &property)
     // have we saturated?
     if((set_union == states).is_true())
     {
-      property.proved();
+      property.proved("BDD");
       message.status() << "Property proved" << messaget::eom;
       break;
     }
@@ -632,7 +632,7 @@ void bdd_enginet::check_CTL(propertyt &property)
   if(intersection.is_false())
   {
     // intersection empty, proved
-    property.proved();
+    property.proved("BDD");
     message.status() << "Property proved" << messaget::eom;
   }
   else
diff --git a/src/ebmc/completeness_threshold.cpp b/src/ebmc/completeness_threshold.cpp
index d029dadeb..e55ab7dee 100644
--- a/src/ebmc/completeness_threshold.cpp
+++ b/src/ebmc/completeness_threshold.cpp
@@ -129,7 +129,7 @@ property_checker_resultt completeness_threshold(
     {
       // Turn "PROVED up to bound k" into "PROVED" if k>=CT
       if(has_low_completeness_threshold(property) && property.bound >= 1)
-        property.proved();
+        property.proved("CT=1");
       else
         property.unknown();
     }
diff --git a/src/ebmc/ebmc_properties.h b/src/ebmc/ebmc_properties.h
index 4f777dd30..67816d047 100644
--- a/src/ebmc/ebmc_properties.h
+++ b/src/ebmc/ebmc_properties.h
@@ -53,6 +53,7 @@ class ebmc_propertiest
     std::size_t bound = 0;
     std::optional<trans_tracet> witness_trace;
     std::optional<std::string> failure_reason;
+    std::optional<std::string> proof_via;
 
     bool has_witness_trace() const
     {
@@ -113,36 +114,49 @@ class ebmc_propertiest
     {
       status = statust::ASSUMED;
       failure_reason = {};
+      proof_via = {};
     }
 
     void unknown()
     {
       status = statust::UNKNOWN;
       failure_reason = {};
+      proof_via = {};
     }
 
     void disable()
     {
       status = statust::DISABLED;
       failure_reason = {};
+      proof_via = {};
     }
 
     void proved()
     {
       status = statust::PROVED;
       failure_reason = {};
+      proof_via = {};
+    }
+
+    void proved(std::string _proof_via)
+    {
+      status = statust::PROVED;
+      failure_reason = {};
+      proof_via = std::move(_proof_via);
     }
 
     void proved_with_bound(std::size_t _bound)
     {
       status = statust::PROVED_WITH_BOUND;
       bound = _bound;
+      proof_via = {};
     }
 
     void refuted()
     {
       status = statust::REFUTED;
       failure_reason = {};
+      proof_via = {};
     }
 
     void refuted_with_bound(std::size_t _bound)
@@ -150,30 +164,35 @@ class ebmc_propertiest
       status = statust::REFUTED_WITH_BOUND;
       bound = _bound;
       failure_reason = {};
+      proof_via = {};
     }
 
     void drop()
     {
       status = statust::DROPPED;
       failure_reason = {};
+      proof_via = {};
     }
 
     void failure(const std::optional<std::string> &reason = {})
     {
       status = statust::FAILURE;
       failure_reason = reason;
+      proof_via = {};
     }
 
     void unsupported(const std::optional<std::string> &reason = {})
     {
       status = statust::UNSUPPORTED;
       failure_reason = reason;
+      proof_via = {};
     }
 
     void inconclusive()
     {
       status = statust::INCONCLUSIVE;
       failure_reason = {};
+      proof_via = {};
     }
 
     std::string status_as_string() const;
diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp
index d7c30dd7b..e91d4a0eb 100644
--- a/src/ebmc/k_induction.cpp
+++ b/src/ebmc/k_induction.cpp
@@ -333,7 +333,7 @@ void k_inductiont::induction_step()
     case decision_proceduret::resultt::D_UNSATISFIABLE:
       message.result() << "UNSAT: inductive proof successful, property holds"
                        << messaget::eom;
-      p_it.proved();
+      p_it.proved(std::to_string(no_timeframes - 1) + "-induction");
       break;
 
     case decision_proceduret::resultt::D_ERROR:
diff --git a/src/ebmc/neural_liveness.cpp b/src/ebmc/neural_liveness.cpp
index e30344884..13aac05a3 100644
--- a/src/ebmc/neural_liveness.cpp
+++ b/src/ebmc/neural_liveness.cpp
@@ -120,7 +120,7 @@ int neural_livenesst::operator()()
   // report outcomes
   const namespacet ns(transition_system.symbol_table);
   property_checker_resultt result{properties};
-  report_results(cmdline, result, ns, message.get_message_handler());
+  report_results(cmdline, false, result, ns, message.get_message_handler());
   return result.exit_code();
 }
 
diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp
index ac6a3e3ed..d18d72921 100644
--- a/src/ebmc/property_checker.cpp
+++ b/src/ebmc/property_checker.cpp
@@ -441,6 +441,10 @@ property_checker_resultt property_checker(
   ebmc_propertiest &properties,
   message_handlert &message_handler)
 {
+  bool use_heuristic_engine = !cmdline.isset("bdd") && !cmdline.isset("aig") &&
+                              !cmdline.isset("k-induction") &&
+                              !cmdline.isset("ic3") && !cmdline.isset("bound");
+
   auto result = [&]() -> property_checker_resultt
   {
     if(cmdline.isset("bdd") || cmdline.isset("show-bdds"))
@@ -485,7 +489,7 @@ property_checker_resultt property_checker(
   if(result.status == property_checker_resultt::statust::VERIFICATION_RESULT)
   {
     const namespacet ns{transition_system.symbol_table};
-    report_results(cmdline, result, ns, message_handler);
+    report_results(cmdline, use_heuristic_engine, result, ns, message_handler);
   }
 
   return result;
diff --git a/src/ebmc/ranking_function.cpp b/src/ebmc/ranking_function.cpp
index d573d1605..2e7ad5ed3 100644
--- a/src/ebmc/ranking_function.cpp
+++ b/src/ebmc/ranking_function.cpp
@@ -128,7 +128,7 @@ int do_ranking_function(
 
   const namespacet ns(transition_system.symbol_table);
   property_checker_resultt checker_result{properties};
-  report_results(cmdline, checker_result, ns, message_handler);
+  report_results(cmdline, false, checker_result, ns, message_handler);
   return checker_result.exit_code();
 }
 
diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp
index 6469c0d9a..e96f97d57 100644
--- a/src/ebmc/report_results.cpp
+++ b/src/ebmc/report_results.cpp
@@ -34,6 +34,7 @@ Function: ebmc_baset::report_results
 
 void report_results(
   const cmdlinet &cmdline,
+  bool show_proof_via,
   const property_checker_resultt &result,
   const namespacet &ns,
   message_handlert &message_handler)
@@ -59,6 +60,9 @@ void report_results(
       if(property.has_witness_trace())
         json_property["trace"] = json(property.witness_trace.value(), ns);
 
+      if(property.is_proved() && property.proof_via.has_value())
+        json_property["proof_via"] = json_stringt{property.proof_via.value()};
+
       json_properties.push_back(std::move(json_property));
     }
 
@@ -81,6 +85,9 @@ void report_results(
       if(property.has_witness_trace())
         xml_result.new_element() = xml(property.witness_trace.value(), ns);
 
+      if(property.is_proved() && property.proof_via.has_value())
+        xml_result.set_attribute("proof_via", property.proof_via.value());
+
       std::cout << xml_result << '\n' << std::flush;
     }
   }
@@ -119,7 +126,16 @@ void report_results(
 
       message.status() << property.status_as_string();
 
-      message.status() << messaget::reset << messaget::eom;
+      message.status() << messaget::reset;
+
+      if(
+        show_proof_via && property.is_proved() &&
+        property.proof_via.has_value())
+      {
+        message.status() << " (" << property.proof_via.value() << ')';
+      }
+
+      message.status() << messaget::eom;
 
       if(property.has_witness_trace())
       {
diff --git a/src/ebmc/report_results.h b/src/ebmc/report_results.h
index 387c1e56e..0cc63942c 100644
--- a/src/ebmc/report_results.h
+++ b/src/ebmc/report_results.h
@@ -19,6 +19,7 @@ class namespacet;
 
 void report_results(
   const cmdlinet &,
+  bool show_proof_via,
   const property_checker_resultt &,
   const namespacet &,
   message_handlert &);