File tree Expand file tree Collapse file tree 2 files changed +17
-3
lines changed
regression/cbmc-incr-oneloop/simpleloop1 Expand file tree Collapse file tree 2 files changed +17
-3
lines changed Original file line number Diff line number Diff line change
1
+ CORE
2
+ main.c
3
+ --incremental-loop main.0 --unwinding-assertions --dimacs
4
+ ^Invalid User Input$
5
+ ^Option: --incremental-loop$
6
+ ^Reason: the chosen solver does not support incremental solving$
7
+ ^EXIT=1$
8
+ ^SIGNAL=0$
9
+ --
10
+ ^warning: ignoring
11
+ ^Unwinding loop
12
+ --
13
+ Test that an appropriate error is shown when using --incremental-loop in
14
+ combination with a solver which does not support incremental solving.
Original file line number Diff line number Diff line change @@ -411,7 +411,7 @@ void solver_factoryt::no_incremental_check()
411
411
{
412
412
const bool all_properties = options.get_bool_option (" all-properties" );
413
413
const bool cover = options.is_set (" cover" );
414
- const bool incremental_check = options.is_set (" incremental-check " );
414
+ const bool incremental_loop = options.is_set (" incremental-loop " );
415
415
416
416
if (all_properties)
417
417
{
@@ -424,10 +424,10 @@ void solver_factoryt::no_incremental_check()
424
424
throw invalid_command_line_argument_exceptiont (
425
425
" the chosen solver does not support incremental solving" , " --cover" );
426
426
}
427
- else if (incremental_check )
427
+ else if (incremental_loop )
428
428
{
429
429
throw invalid_command_line_argument_exceptiont (
430
430
" the chosen solver does not support incremental solving" ,
431
- " --incremental-check " );
431
+ " --incremental-loop " );
432
432
}
433
433
}
You can’t perform that action at this time.
0 commit comments