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 witness_trace; std::optional failure_reason; + std::optional 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 &reason = {}) { status = statust::FAILURE; failure_reason = reason; + proof_via = {}; } void unsupported(const std::optional &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 &);