IllegalArgumentException: unknown symbol (const Int (Array Int Int))

[danieldietsch]

Version c3a52b3
File loops/nec40.c
Severity: occurs on 11 of 2310 (https://struebli.informatik.uni-freiburg.de/logs/student-acceleration/20210416-091202-student-acceleration-259539aefe-M/overview)

Stacktrace

java.lang.IllegalArgumentException: unknown symbol (const Int (Array Int Int))
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Term2Expression.translate(Term2Expression.java:240)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Term2Expression.translate(Term2Expression.java:129)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Term2Expression.translate(Term2Expression.java:165)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Term2Expression.translate(Term2Expression.java:129)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Term2Expression.translate(Term2Expression.java:165)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Term2Expression.translate(Term2Expression.java:129)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Term2Expression.translate(Term2Expression.java:165)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Term2Expression.translate(Term2Expression.java:129)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.RCFGBacktranslator.translateExpression(RCFGBacktranslator.java:394)
...

Log:
https://struebli.informatik.uni-freiburg.de/logs/student-acceleration/20210416-091202-student-acceleration-259539aefe-M/student-acceleration.2021-04-15_22-53-33.logfiles/Automizer%20AcceleratedInterpolation%20Jordan.nec40.yml.log

[Heizmann]

The problem is that we don't know how to backtranslate ((as const (Array Int Int)) 0) from SMT to Boogie.

Here, this term occurs as a subterm of (= (select |#memory_int| |~#x~0.base|) ((as const (Array Int Int)) 0)) in some invariant. The invariant should state that the memory segment at the pointer |~#x~0.base| is full of zeros.

[danieldietsch]

I have an idea, but it will take me until after 15th to fix it.