From a62499a42668146fe9b33da955452cf220cad355 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 30 Sep 2024 11:33:57 -0700 Subject: [PATCH] fix property ID in the ranking benchmarks Assertions now go into the scope without "property." prefix. --- examples/Benchmarks/check_ranking | 60 +++++++++++++++---------------- 1 file changed, 30 insertions(+), 30 deletions(-) diff --git a/examples/Benchmarks/check_ranking b/examples/Benchmarks/check_ranking index 664800675..1d680fe94 100755 --- a/examples/Benchmarks/check_ranking +++ b/examples/Benchmarks/check_ranking @@ -77,37 +77,37 @@ ebmc lcd_12.sv --ranking-function "{3-state,22500-cnt}" ebmc lcd_13.sv --ranking-function "{3-state,90000-cnt}" ebmc lcd_14.sv --ranking-function "{3-state,180000-cnt}" -ebmc seven_seg_1.sv --ranking-function "250-cnt" --property SEVEN.property.p1 -ebmc seven_seg_2.sv --ranking-function "500-cnt" --property SEVEN.property.p1 -ebmc seven_seg_3.sv --ranking-function "750-cnt" --property SEVEN.property.p1 -ebmc seven_seg_4.sv --ranking-function "1000-cnt" --property SEVEN.property.p1 -ebmc seven_seg_5.sv --ranking-function "2500-cnt" --property SEVEN.property.p1 -ebmc seven_seg_6.sv --ranking-function "5000-cnt" --property SEVEN.property.p1 -ebmc seven_seg_7.sv --ranking-function "7500-cnt" --property SEVEN.property.p1 -ebmc seven_seg_8.sv --ranking-function "10000-cnt" --property SEVEN.property.p1 -ebmc seven_seg_9.sv --ranking-function "12500-cnt" --property SEVEN.property.p1 -ebmc seven_seg_10.sv --ranking-function "15000-cnt" --property SEVEN.property.p1 -ebmc seven_seg_11.sv --ranking-function "17500-cnt" --property SEVEN.property.p1 -ebmc seven_seg_12.sv --ranking-function "20000-cnt" --property SEVEN.property.p1 -ebmc seven_seg_16.sv --ranking-function "40000-cnt" --property SEVEN.property.p1 -ebmc seven_seg_17.sv --ranking-function "80000-cnt" --property SEVEN.property.p1 -ebmc seven_seg_18.sv --ranking-function "160000-cnt" --property SEVEN.property.p1 +ebmc seven_seg_1.sv --ranking-function "250-cnt" --property SEVEN.p1 +ebmc seven_seg_2.sv --ranking-function "500-cnt" --property SEVEN.p1 +ebmc seven_seg_3.sv --ranking-function "750-cnt" --property SEVEN.p1 +ebmc seven_seg_4.sv --ranking-function "1000-cnt" --property SEVEN.p1 +ebmc seven_seg_5.sv --ranking-function "2500-cnt" --property SEVEN.p1 +ebmc seven_seg_6.sv --ranking-function "5000-cnt" --property SEVEN.p1 +ebmc seven_seg_7.sv --ranking-function "7500-cnt" --property SEVEN.p1 +ebmc seven_seg_8.sv --ranking-function "10000-cnt" --property SEVEN.p1 +ebmc seven_seg_9.sv --ranking-function "12500-cnt" --property SEVEN.p1 +ebmc seven_seg_10.sv --ranking-function "15000-cnt" --property SEVEN.p1 +ebmc seven_seg_11.sv --ranking-function "17500-cnt" --property SEVEN.p1 +ebmc seven_seg_12.sv --ranking-function "20000-cnt" --property SEVEN.p1 +ebmc seven_seg_16.sv --ranking-function "40000-cnt" --property SEVEN.p1 +ebmc seven_seg_17.sv --ranking-function "80000-cnt" --property SEVEN.p1 +ebmc seven_seg_18.sv --ranking-function "160000-cnt" --property SEVEN.p1 -ebmc seven_seg_1.sv --ranking-function "250-cnt" --property SEVEN.property.p2 -ebmc seven_seg_2.sv --ranking-function "500-cnt" --property SEVEN.property.p2 -ebmc seven_seg_3.sv --ranking-function "750-cnt" --property SEVEN.property.p2 -ebmc seven_seg_4.sv --ranking-function "1000-cnt" --property SEVEN.property.p2 -ebmc seven_seg_5.sv --ranking-function "2500-cnt" --property SEVEN.property.p2 -ebmc seven_seg_6.sv --ranking-function "5000-cnt" --property SEVEN.property.p2 -ebmc seven_seg_7.sv --ranking-function "7500-cnt" --property SEVEN.property.p2 -ebmc seven_seg_8.sv --ranking-function "10000-cnt" --property SEVEN.property.p2 -ebmc seven_seg_9.sv --ranking-function "12500-cnt" --property SEVEN.property.p2 -ebmc seven_seg_10.sv --ranking-function "15000-cnt" --property SEVEN.property.p2 -ebmc seven_seg_11.sv --ranking-function "17500-cnt" --property SEVEN.property.p2 -ebmc seven_seg_12.sv --ranking-function "20000-cnt" --property SEVEN.property.p2 -ebmc seven_seg_16.sv --ranking-function "40000-cnt" --property SEVEN.property.p2 -ebmc seven_seg_17.sv --ranking-function "80000-cnt" --property SEVEN.property.p2 -ebmc seven_seg_18.sv --ranking-function "160000-cnt" --property SEVEN.property.p2 +ebmc seven_seg_1.sv --ranking-function "250-cnt" --property SEVEN.p2 +ebmc seven_seg_2.sv --ranking-function "500-cnt" --property SEVEN.p2 +ebmc seven_seg_3.sv --ranking-function "750-cnt" --property SEVEN.p2 +ebmc seven_seg_4.sv --ranking-function "1000-cnt" --property SEVEN.p2 +ebmc seven_seg_5.sv --ranking-function "2500-cnt" --property SEVEN.p2 +ebmc seven_seg_6.sv --ranking-function "5000-cnt" --property SEVEN.p2 +ebmc seven_seg_7.sv --ranking-function "7500-cnt" --property SEVEN.p2 +ebmc seven_seg_8.sv --ranking-function "10000-cnt" --property SEVEN.p2 +ebmc seven_seg_9.sv --ranking-function "12500-cnt" --property SEVEN.p2 +ebmc seven_seg_10.sv --ranking-function "15000-cnt" --property SEVEN.p2 +ebmc seven_seg_11.sv --ranking-function "17500-cnt" --property SEVEN.p2 +ebmc seven_seg_12.sv --ranking-function "20000-cnt" --property SEVEN.p2 +ebmc seven_seg_16.sv --ranking-function "40000-cnt" --property SEVEN.p2 +ebmc seven_seg_17.sv --ranking-function "80000-cnt" --property SEVEN.p2 +ebmc seven_seg_18.sv --ranking-function "160000-cnt" --property SEVEN.p2 ebmc thermocouple_1.sv --ranking-function "{2-state,2**5-cnt}" ebmc thermocouple_2.sv --ranking-function "{2-state,2**9-cnt}"