fx

Author: kroening

regression/ebmc/neural-liveness/counter1.desc

@@ -1,6 +1,6 @@
 CORE
 counter1.sv
---number-of-traces 2 --neural-liveness --neural-engine "echo RESULT: counter\\\\n"
+--traces 2 --neural-liveness --neural-engine "echo RESULT: counter\\\\n"
 ^\[main\.property\.p0\] always s_eventually main.counter == 0: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$

regression/ebmc/neural-liveness/live_signal1.desc

@@ -1,6 +1,6 @@
 CORE
 counter1.sv
---number-of-traces 1 --neural-liveness --show-traces
+--traces 1 --neural-liveness --show-traces
 ^Verilog::main\.\$live@0 = 0$
 ^Verilog::main\.\$live@1 = 0$
 ^Verilog::main\.\$live@2 = 0$

regression/ebmc/random-traces/boolean1.desc

@@ -1,6 +1,6 @@
 CORE broken-smt-backend
 boolean1.v
---random-traces --trace-steps 0 --number-of-traces 2
+--random-traces --trace-steps 0 --traces 2
 ^\*\*\* Trace 1$
 ^  main\.some_wire = 0$
 ^  main\.input1 = 0$

regression/ebmc/random-traces/bv1.desc

@@ -1,6 +1,6 @@
 CORE broken-smt-backend
 bv1.v
---random-traces --trace-steps 1 --number-of-traces 1
+--random-traces --trace-steps 1 --traces 1
 ^Transition system state 0$
 ^  main\.some_reg = 0 .*$
 ^  main\.input1 = 'h6FE4167A .*$

regression/ebmc/random-traces/counter_with_initial_value.desc

@@ -1,6 +1,6 @@
 CORE broken-smt-backend
 counter_with_initial_value.v
---random-traces --trace-steps 10 --waveform --number-of-traces 2
+--random-traces --trace-steps 10 --waveform --traces 2
 ^\*\*\* Trace 1$
 ^                0   1   2   3   4   5   6   7   8   9  10$
 ^     main.clk                                            $

regression/ebmc/random-traces/long_trace1.desc

@@ -1,6 +1,6 @@
 CORE broken-smt-backend
 long_trace1.v
---random-traces --number-of-traces 1 --trace-steps 1000
+--random-traces --traces 1 --trace-steps 1000
 ^Transition system state 0$
 ^  main\.some_reg = 0 .*$
 ^  main\.increment = 0$

regression/ebmc/random-traces/with_submodule.desc

@@ -1,6 +1,6 @@
 CORE broken-smt-backend
 with_submodule.v
---random-traces --trace-steps 0 --number-of-traces 2
+--random-traces --trace-steps 0 --traces 2
 ^\*\*\* Trace 1$
 ^  main\.some_wire = 0$
 ^  main\.input1 = 0$

src/ebmc/ebmc_parse_options.cpp

@@ -375,7 +375,7 @@ void ebmc_parse_optionst::help()
     "    {y--new-mode}               \t new mode is switched on\n"
     "    {y--aiger}                  \t print out the instance in aiger format\n"
     " {y--random-traces}             \t generate random traces\n"
-    "    {y--number-of-traces} {unumber}\t generate the given number of traces\n"
+    "    {y--traces} {unumber}       \t generate the given number of traces\n"
     "    {y--random-seed} {unumber}  \t use the given random seed\n"
     "    {y--trace-steps} {unumber}  \t set the number of random transitions (default: 10 steps)\n"
     " {y--random-trace}              \t generate a random trace\n"

src/ebmc/ebmc_parse_options.h

@@ -43,7 +43,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(smt2)(bitwuzla)(boolector)(cvc3)(cvc4)(cvc5)(mathsat)(yices)(z3)"
         "(aig)(stop-induction)(stop-minimize)(start):(coverage)(naive)"
         "(compute-ct)(dot-netlist)(smv-netlist)(vcd):"
-        "(random-traces)(trace-steps):(random-seed):(number-of-traces):"
+        "(random-traces)(trace-steps):(random-seed):(traces):"
         "(random-trace)(random-waveform)"
         "(liveness-to-safety)"
         "I:(preprocess)(systemverilog)(vl2smv-extensions)",

src/ebmc/neural_liveness.cpp

@@ -212,10 +212,10 @@ void neural_livenesst::sample(std::function<void(trans_tracet)> trace_consumer)
 {
   const auto number_of_traces = [this]() -> std::size_t
   {
-    if(cmdline.isset("number-of-traces"))
+    if(cmdline.isset("traces"))
     {
       auto number_of_traces_opt =
-        string2optional_size_t(cmdline.get_value("number-of-traces"));
+        string2optional_size_t(cmdline.get_value("traces"));
 
       if(!number_of_traces_opt.has_value())
         throw ebmc_errort() << "failed to parse number of traces";