NegativeArraySizeException in DualJunctionTir$ExplicitLhsPolynomialRelations.buildDualFiniteJunction

[danieldietsch]

Version c3a52b3
File nla-digbench-scaling/hard-u_unwindbound5.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.NegativeArraySizeException: -1072721305
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir$ExplicitLhsPolynomialRelations.buildDualFiniteJunction(DualJunctionTir.java:651)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir$ExplicitLhsPolynomialRelations.buildCorrespondingFiniteJunctionForAntiDer(DualJunctionTir.java:615)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir$ExplicitLhsPolynomialRelations.buildBoundConstraint(DualJunctionTir.java:451)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir.tryToEliminateConjuncts(DualJunctionTir.java:205)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir.tryToEliminateOne(DualJunctionTir.java:160)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir.tryExhaustivelyToEliminate(DualJunctionTir.java:125)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir.tryToEliminate(DualJunctionTir.java:112)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher.tryToEliminateOne(QuantifierPusher.java:862)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher.applyNewEliminationTechniquesExhaustively(QuantifierPusher.java:828)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher.applyDualJunctionEliminationTechniques(QuantifierPusher.java:746)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher.tryToPushOverDualFiniteConnective2(QuantifierPusher.java:383)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher.tryToPushOverDualFiniteConnective(QuantifierPusher.java:315)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher.convert(QuantifierPusher.java:227)
	at de.uni_freiburg.informatik.ultimate.logic.TermTransformer.cacheConvert(TermTransformer.java:131)
	at de.uni_freiburg.informatik.ultimate.logic.TermTransformer$Convert.walk(TermTransformer.java:79)
	at de.uni_freiburg.informatik.ultimate.logic.NonRecursive.run(NonRecursive.java:115)
	at de.uni_freiburg.informatik.ultimate.logic.NonRecursive.run(NonRecursive.java:106)
	at de.uni_freiburg.informatik.ultimate.logic.TermTransformer.transform(TermTransformer.java:272)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher.eliminate(QuantifierPusher.java:144)
...

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%20IcfgTranformation%20Jordan.hard-u_unwindbound5.yml.log

[Heizmann]

I cannot fix this problem soon.