Skip to content

Commit fdbbf7e

Browse files
author
Thomas Kiley
committed
Tweak where we print the incremental status
We want to print the status after we've done any solving for that unwind, but before we've done an extra step of symexing. We should not print in the event the full equation has been generated, as then we have a full solution so ins't incremental. Ditto we don't need to print the status if we've found a failure, as this function will be called again to do the next symex invocation if there are further propreties to check
1 parent 22bce6f commit fdbbf7e

File tree

1 file changed

+2
-4
lines changed

1 file changed

+2
-4
lines changed

src/goto-checker/single_loop_incremental_symex_checker.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -81,8 +81,6 @@ operator()(propertiest &properties)
8181
update_properties_status_from_symex_target_equation(
8282
properties, result.updated_properties, equation);
8383

84-
output_incremental_status(properties, log);
85-
8684
initial_equation_generated = true;
8785
}
8886

@@ -171,6 +169,8 @@ operator()(propertiest &properties)
171169
break;
172170
}
173171

172+
output_incremental_status(properties, log);
173+
174174
// We continue symbolic execution
175175
full_equation_generated =
176176
!symex.resume(goto_symext::get_goto_function(goto_model));
@@ -181,8 +181,6 @@ operator()(propertiest &properties)
181181
properties, result.updated_properties, equation);
182182

183183
current_equation_converted = false;
184-
185-
output_incremental_status(properties, log);
186184
}
187185

188186
return result;

0 commit comments

Comments
 (0)