diff --git a/regression/ebmc/neural-liveness/counter1.desc b/regression/ebmc/neural-liveness/counter1.desc index 55f0ccc5a..da00acbd7 100644 --- a/regression/ebmc/neural-liveness/counter1.desc +++ b/regression/ebmc/neural-liveness/counter1.desc @@ -1,6 +1,6 @@ CORE counter1.sv ---number-of-traces 2 --neural-liveness --neural-engine "echo Candidate: counter\\\\n" +--traces 2 --neural-liveness --neural-engine "echo Candidate: counter\\\\n" ^\[main\.property\.p0\] always s_eventually main.counter == 0: PROVED$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/ebmc/neural-liveness/live_signal1.desc b/regression/ebmc/neural-liveness/live_signal1.desc index 8a3768dd8..233ba63db 100644 --- a/regression/ebmc/neural-liveness/live_signal1.desc +++ b/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 ^nuterm::live@0 = 0$ ^nuterm::live@1 = 0$ ^nuterm::live@2 = 0$ diff --git a/regression/ebmc/random-traces/boolean1.desc b/regression/ebmc/random-traces/boolean1.desc index b6e61f36f..ff4883e3f 100644 --- a/regression/ebmc/random-traces/boolean1.desc +++ b/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$ diff --git a/regression/ebmc/random-traces/bv1.desc b/regression/ebmc/random-traces/bv1.desc index adf3a7eab..65e2429b8 100644 --- a/regression/ebmc/random-traces/bv1.desc +++ b/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 .*$ diff --git a/regression/ebmc/random-traces/counter_with_initial_value.desc b/regression/ebmc/random-traces/counter_with_initial_value.desc index 7f8b1f1fe..01fc2376a 100644 --- a/regression/ebmc/random-traces/counter_with_initial_value.desc +++ b/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 $ diff --git a/regression/ebmc/random-traces/long_trace1.desc b/regression/ebmc/random-traces/long_trace1.desc index 4fa67a635..fa5813408 100644 --- a/regression/ebmc/random-traces/long_trace1.desc +++ b/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$ diff --git a/regression/ebmc/random-traces/with_submodule.desc b/regression/ebmc/random-traces/with_submodule.desc index 51672d398..0a4c5fb54 100644 --- a/regression/ebmc/random-traces/with_submodule.desc +++ b/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$ diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 40b94cc38..d1029b152 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/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" diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index 605fa03c8..29e45304e 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/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)", diff --git a/src/ebmc/neural_liveness.cpp b/src/ebmc/neural_liveness.cpp index 3c897a570..d54eb1ce9 100644 --- a/src/ebmc/neural_liveness.cpp +++ b/src/ebmc/neural_liveness.cpp @@ -211,12 +211,11 @@ neural_livenesst::dump_vcd_files(temp_dirt &temp_dir) void neural_livenesst::sample(std::function trace_consumer) { - const auto number_of_traces = [this]() -> std::size_t - { - if(cmdline.isset("number-of-traces")) + const auto number_of_traces = [this]() -> std::size_t { + 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"; diff --git a/src/ebmc/random_traces.cpp b/src/ebmc/random_traces.cpp index f284adb3a..8def46279 100644 --- a/src/ebmc/random_traces.cpp +++ b/src/ebmc/random_traces.cpp @@ -112,12 +112,11 @@ Function: random_traces int random_traces(const cmdlinet &cmdline, message_handlert &message_handler) { - const auto number_of_traces = [&cmdline]() -> std::size_t - { - if(cmdline.isset("number-of-traces")) + const auto number_of_traces = [&cmdline]() -> std::size_t { + 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"; @@ -233,8 +232,8 @@ Function: random_trace int random_trace(const cmdlinet &cmdline, message_handlert &message_handler) { - if(cmdline.isset("number-of-traces")) - throw ebmc_errort() << "must not give number-of-traces"; + if(cmdline.isset("traces")) + throw ebmc_errort() << "must not give number of traces"; const std::size_t random_seed = [&cmdline]() -> std::size_t { if(cmdline.isset("random-seed"))