diff --git a/regression/ebmc/ranking-function/counter_with_reset1.fail.desc b/regression/ebmc/ranking-function/counter_with_reset1.fail.desc
new file mode 100644
index 000000000..a491014ff
--- /dev/null
+++ b/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$
+--
diff --git a/regression/ebmc/ranking-function/counter_with_reset1.pass.desc b/regression/ebmc/ranking-function/counter_with_reset1.pass.desc
new file mode 100644
index 000000000..523ee0f14
--- /dev/null
+++ b/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$
+--
diff --git a/regression/ebmc/ranking-function/counter_with_reset1.sv b/regression/ebmc/ranking-function/counter_with_reset1.sv
new file mode 100644
index 000000000..26e90267b
--- /dev/null
+++ b/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
diff --git a/src/ebmc/ranking_function.cpp b/src/ebmc/ranking_function.cpp
index 33a5a8173..81c78aaec 100644
--- a/src/ebmc/ranking_function.cpp
+++ b/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);