Open
Description
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.