Skip to content

Commit d2e3959

Browse files
Add SSA validation
1 parent 2eb7294 commit d2e3959

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

src/goto-checker/multi_path_symex_only_checker.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,11 @@ void multi_path_symex_only_checkert::perform_symex()
8989
<< equation.SSA_steps.size() << " steps" << messaget::eom;
9090

9191
slice(symex, equation, ns, options, ui_message_handler);
92+
93+
if(options.get_bool_option("validate-ssa-equation"))
94+
{
95+
symex.validate(validation_modet::INVARIANT);
96+
}
9297
}
9398

9499
void multi_path_symex_only_checkert::output_coverage_report()

0 commit comments

Comments
 (0)