Merge pull request #225 from diffblue/ranking-function-property

ebmc: --ranking-function now honors --property

regression/ebmc/ranking-function/counter_with_reset1.fail.desc

@@ -0,0 +1,7 @@
+CORE
+counter_with_reset1.sv
+--property main.property.p0 --ranking-function 10-counter
+^\[main\.property\.p0\] always \(eventually main.counter == 10\): UNKNOWN$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/ranking-function/counter_with_reset1.pass.desc

@@ -0,0 +1,7 @@
+CORE
+counter_with_reset1.sv
+--property main.property.p1 --ranking-function 10-counter
+^\[main\.property\.p1\] always \(eventually main.reset \|\| main.counter == 10\): SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/ranking-function/counter_with_reset1.sv

@@ -0,0 +1,21 @@
+// count up from 0 to 10
+
+module main(input clk, input reset);
+
+  reg [3:0] counter;
+
+  initial counter = 0;
+
+  always @(posedge clk)
+    if(reset)
+      counter = 0;
+    else if(counter != 10)
+      counter = counter + 1;
+
+  // expected to fail, owing to reset
+  p0: assert property (eventually counter == 10);
+
+  // expected to pass
+  p1: assert property (eventually (reset || counter == 10));
+
+endmodule

src/ebmc/ranking_function.cpp

@@ -102,8 +102,8 @@ int do_ranking_function(
     cmdline.get_value("ranking-function"), transition_system, message_handler);
 
   // find the property
-  auto properties = ebmc_propertiest::from_transition_system(
-    transition_system, message_handler);
+  auto properties = ebmc_propertiest::from_command_line(
+    cmdline, transition_system, message_handler);
 
   auto &property = find_property(properties);