Skip to content

Commit

Permalink
IC3: better error message when given assumption
Browse files Browse the repository at this point in the history
This improves the error handling when giving an assumption to the IC3 engine.
  • Loading branch information
kroening committed Dec 26, 2024
1 parent 7ae93d8 commit f277eb6
Show file tree
Hide file tree
Showing 3 changed files with 30 additions and 0 deletions.
7 changes: 7 additions & 0 deletions regression/ebmc/ic3/not_supported3.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
not_supported3.sv
--ic3
^no support for assumptions$
^EXIT=1$
^SIGNAL=0$
--
13 changes: 13 additions & 0 deletions regression/ebmc/ic3/not_supported3.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
module main(input clk);

reg my_bit;

initial my_bit=0;

always @(posedge clk)
my_bit = !my_bit;

// no support for assumptions
p0: assume property (my_bit == 0);

endmodule
10 changes: 10 additions & 0 deletions src/ic3/m1ain.cc
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,16 @@ int ic3_enginet::operator()()
return 1;
}

// No support for assumptions
for(auto &property : properties.properties)
{
if(property.is_assumed())
{
message.error() << "no support for assumptions" << messaget::eom;
return 1;
}
}

std::size_t number_of_properties = 0;

for(auto &property : properties.properties)
Expand Down

0 comments on commit f277eb6

Please sign in to comment.