CBMC version: 5.6 and 5.12 (cbmc-5.12-206-g873daa903)
Operating system: Ubuntu 18.04.4 LTS (64bits), gcc 7.5.0
Exact command line resulting in the issue:

goto-cc test.c -o binary.gb
goto-instrument binary.gb --k-induction 5 --step-case step_case.gb

What behaviour did you expect: the k-induction instrumentation to occur
What happened instead: Segmentation fault (core-dumped)

Greetings,

I encountered a crash while instrumenting the k-induction step case on the following program:

test.c

int nondet_condition();  
int main()
{ 
	int i=0;   
	int j=0;        
	while(i<10)                 
	{                                 
		while(nondet_condition() == 0)           
		{                                                
			j++;                                                       
			if(j==10) j=0;                          
		}                             
		__CPROVER_assert(j < 11, "should hold");      
		i++;                      
	}                      
}                                                       

'Compiling' gives the following:

user@pc:/$ goto-cc test.c -o binary.gb
user@pc:/$ goto-instrument binary.gb --k-induction 5 --step-case step_case.gb
Reading GOTO program from `binary.gb'
Instrumenting k-induction for k=5, step case
Segmentation fault (core dumped)
user@pc:/$

After trying out different variants of the code above, I think that the crash occurs for any program containing nested loops (a while within a while).

The crash does not occur on the --base-case of the k-induction.