Skip to content

Commit c63e328

Browse files
committed
Add goto-convert before verifying candidate
1 parent fdea352 commit c63e328

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

src/goto-instrument/synthesizer/cegis_verifier.cpp

+6
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Author: Qinheping Hu
1717
#include <util/pointer_predicates.h>
1818
#include <util/prefix.h>
1919

20+
#include <goto-programs/goto_convert_functions.h>
2021
#include <goto-programs/link_to_library.h>
2122
#include <goto-programs/pointer_arithmetic.h>
2223
#include <goto-programs/process_goto_program.h>
@@ -392,6 +393,11 @@ bool cegis_verifiert::verify()
392393
all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>>(
393394
options, ui_message_handler, goto_model);
394395

396+
goto_convert(
397+
goto_model.symbol_table,
398+
goto_model.goto_functions,
399+
log.get_message_handler());
400+
395401
// Run the checker to get the result.
396402
const resultt result = (*checker)();
397403

0 commit comments

Comments
 (0)