Skip to content

Commit bac2bde

Browse files
committed
Use make_assumption/assertion wrappers
instead of instructiont constructor. Also a bit of clang-formatting.
1 parent ae54fcc commit bac2bde

File tree

1 file changed

+6
-10
lines changed

1 file changed

+6
-10
lines changed

src/analyses/goto_check.cpp

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1490,20 +1490,16 @@ void goto_checkt::add_guarded_claim(
14901490

14911491
if(assertions.insert(guarded_expr).second)
14921492
{
1493-
goto_program_instruction_typet type=
1494-
enable_assert_to_assume?ASSUME:ASSERT;
1495-
1496-
goto_programt::targett t = new_code.add(goto_programt::instructiont(
1497-
static_cast<const codet &>(get_nil_irep()),
1498-
source_location,
1499-
type,
1500-
std::move(guarded_expr),
1501-
{}));
1493+
auto t = new_code.add(
1494+
enable_assert_to_assume ? goto_programt::make_assumption(
1495+
std::move(guarded_expr), source_location)
1496+
: goto_programt::make_assertion(
1497+
std::move(guarded_expr), source_location));
15021498

15031499
std::string source_expr_string;
15041500
get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
15051501

1506-
t->source_location.set_comment(comment+" in "+source_expr_string);
1502+
t->source_location.set_comment(comment + " in " + source_expr_string);
15071503
t->source_location.set_property_class(property_class);
15081504
}
15091505
}

0 commit comments

Comments
 (0)