Skip to content

Commit 942d70e

Browse files
Initialise message_handler in bv_refinement unit test
The message_handler member of bv_refinementt::infot was left uninitialised, which is undefined behaviour when it is later dereferenced. Set it to null_message_handler. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
1 parent 7a4df92 commit 942d70e

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -171,6 +171,7 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
171171
bv_refinementt::infot info;
172172
info.ns = &ns;
173173
info.prop = &sat_check;
174+
info.message_handler = &null_message_handler;
174175
info.output_xml = false;
175176
bv_refinementt solver(info);
176177
solver << expr;

0 commit comments

Comments
 (0)