Bug #7992
closedRSB fails at witnesses processing during validation run
0%
Description
Currently there are 5 unsafes cannot be visualized after the run of the validation set (d8e172f3c0a5, 448356262f56~, 214c97a12f1f, c822fb57ba12, c822fb57ba12~) due to error at RSB:
Traceback (most recent call last):
File "/work/zakharov/src/klever/core/core/components.py", line 116, in run
self.main()
File "/work/zakharov/src/klever/core/core/utils.py", line 56, in callbacks_caller
ret = attr(*args, **kwargs)
File "/work/zakharov/src/klever/core/core/vtg/rsb.py", line 46, in generate_verification_tasks
self.decide_verification_task()
File "/work/zakharov/src/klever/core/core/utils.py", line 56, in callbacks_caller
ret = attr(*args, **kwargs)
File "/work/zakharov/src/klever/core/core/vtg/rsb.py", line 318, in decide_verification_task
self.process_single_verdict(decision_results, verification_report_id)
File "/work/zakharov/src/klever/core/core/utils.py", line 56, in callbacks_caller
ret = attr(*args, **kwargs)
File "/work/zakharov/src/klever/core/core/vtg/rsb.py", line 409, in process_single_verdict
et = import_error_trace(self.logger, witnesses0)
File "/work/zakharov/src/klever/core/core/vtg/et/__init__.py", line 32, in import_error_trace
generic_simplifications(logger, trace)
File "/work/zakharov/src/klever/core/core/vtg/et/tmpvars.py", line 25, in generic_simplifications
_remove_aux_functions(logger, trace)
File "/work/zakharov/src/klever/core/core/vtg/et/tmpvars.py", line 287, in _remove_aux_functions
actual_args[i] = aux_actual_args[j]
IndexError: list index out of range
Updated by Evgeny Novikov about 7 years ago
- Status changed from New to Closed
I fixed this in a47d838 to master. So now all 5 mentioned unsafes can be pretty found.