Skip to content

Commit

Permalink
EBMC: retain assumptions when using --property
Browse files Browse the repository at this point in the history
When using the --property command-line option, do not disable the
assumptions.
  • Loading branch information
kroening committed Oct 18, 2024
1 parent 88a0e54 commit 8f647c5
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 1 deletion.
1 change: 1 addition & 0 deletions CHANGELOG
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
* Verilog: allow indexed part select
* word-level BMC: fix for F/s_eventually and U/s_until
* IC3: liveness to safety translation
* Assumptions are not disabled when using --property

# EBMC 5.2

Expand Down
4 changes: 3 additions & 1 deletion src/ebmc/ebmc_properties.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -110,8 +110,10 @@ bool ebmc_propertiest::select_property(
{
std::string property = cmdline.get_value("property");

// disable all assertions (not: assumptions)
for(auto &p : properties)
p.status = propertyt::statust::DISABLED;
if(!p.is_assumed())
p.status = propertyt::statust::DISABLED;

bool found = false;

Expand Down

0 comments on commit 8f647c5

Please sign in to comment.