Skip to content

Commit e873e00

Browse files
author
thk123
committed
Correcting assertions
Removing an assertion that validates the STL lib being correct. Changed assert to invariant that all components on a struct have a name.
1 parent 0547fae commit e873e00

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

src/java_bytecode/java_object_factory.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -365,7 +365,6 @@ void java_object_factoryt::gen_nondet_struct_init(
365365
class_identifier=struct_tag;
366366

367367
recursion_set.insert(struct_tag);
368-
assert(!recursion_set.empty());
369368

370369
for(const auto &component : components)
371370
{
@@ -390,7 +389,7 @@ void java_object_factoryt::gen_nondet_struct_init(
390389
}
391390
else
392391
{
393-
assert(!name.empty());
392+
INVARIANT(!name.empty(), "Each component of a struct must have a name");
394393

395394
bool _is_sub=name[0]=='@';
396395

0 commit comments

Comments
 (0)