Inductivity Fails when using Accelerated Interpolation for programs with asserts in loops

[JonasWerner]

Version b4afca6
File examples\programs\acceleratedInterpolation\assertionError\oneLoopAssertionError.bpl

When checking this program with accelerated interpolation using either setting in
examples\settings\automizer\acceleratedInterpolation

We get an inductivity failed assertion error:

Transition 89#(exists ((v_main_x_10 Int)) (and (<= 0 v_main_x_10) (<= v_main_x_10 0) (or (and (<= (+ v_main_x_10 4) main_x) (<= (* 2 main_x) 6) (<= main_x 4)) (and (<= (* 2 main_x) 6) (<= (+ v_main_x_10 2) main_x) (<= main_x (+ v_main_x_10 2))) (= main_x (+ v_main_x_10 1))))) ( _ , assume x <= 4; , 86#(<= main_x 1) ) not inductive
Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
The Plugin de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction has thrown an exception:
java.lang.AssertionError: inductivity failed

I assume these errors stem from the assert in the loop, as they are the only programs that are still unsound in #550

For example:
sv-benchmarks\c\loop-invgen\MADWiFi-encode_ie_ok
suffers from the same bug.

[danieldietsch]

Seems to be fixed with 70eefee

@jonas Can you confirm that examples\programs\acceleratedInterpolation\assertionError\oneLoopAssertionError.bpl is fixed and close the ticket?