Skip to content

Commit 8a06eea

Browse files
Replace fallback by error message
All bmct functionality has now been replaced by goto checker infrastructure.
1 parent eca9530 commit 8a06eea

File tree

3 files changed

+4
-507
lines changed

3 files changed

+4
-507
lines changed

src/cbmc/cbmc_parse_options.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -669,11 +669,12 @@ int cbmc_parse_optionst::doit()
669669
}
670670
}
671671

672-
// fall back until everything has been ported to goto-checker
672+
// We should know now which verifier to execute.
673673
if(verifier == nullptr)
674674
{
675-
return bmct::do_language_agnostic_bmc(
676-
options, goto_model, ui_message_handler);
675+
error() << "Given combination of command line arguments not supported"
676+
<< eom;
677+
exit(CPROVER_EXIT_USAGE_ERROR);
677678
}
678679

679680
resultt result = (*verifier)();

0 commit comments

Comments
 (0)