Skip to content

Commit eca4f07

Browse files
Add SSA validation
1 parent 997f125 commit eca4f07

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
@@ -88,6 +88,11 @@ void multi_path_symex_only_checkert::perform_symex()
8888
<< equation.SSA_steps.size() << " steps" << messaget::eom;
8989

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

9398
void multi_path_symex_only_checkert::output_coverage_report()

0 commit comments

Comments
 (0)