diff --git a/regression/ebmc/p-command-line-option/p-command-line-option1.desc b/regression/ebmc/p-command-line-option/p-command-line-option1.desc new file mode 100644 index 000000000..96c73fb30 --- /dev/null +++ b/regression/ebmc/p-command-line-option/p-command-line-option1.desc @@ -0,0 +1,8 @@ +CORE +p-command-line-option1.v +--bound 1 -p "some_value >= 1" +^EXIT=0$ +^SIGNAL=0$ +^\[command-line assertion\] always main\.some_value >= 1: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/ebmc/p-command-line-option/p-command-line-option1.v b/regression/ebmc/p-command-line-option/p-command-line-option1.v new file mode 100644 index 000000000..d4673ea5f --- /dev/null +++ b/regression/ebmc/p-command-line-option/p-command-line-option1.v @@ -0,0 +1,10 @@ +module main(input clk); + + reg [31:0] some_value; + + initial some_value = 1; + + always @(posedge clk) + some_value = some_value + 1; + +endmodule diff --git a/src/ebmc/ebmc_properties.cpp b/src/ebmc/ebmc_properties.cpp index 802b0898c..0d78181ae 100644 --- a/src/ebmc/ebmc_properties.cpp +++ b/src/ebmc/ebmc_properties.cpp @@ -104,6 +104,8 @@ ebmc_propertiest ebmc_propertiest::from_command_line( auto property_string = cmdline.get_value('p'); + language->set_message_handler(message_handler); + exprt expr; if(language->to_expr( property_string,