Skip to content

CIF data-based synthesis crashes when node array gets too big

I got a crash report that looks like this:

java.lang.NegativeArraySizeException: -2130973901
	at com.github.javabdd.JFactory.doResize(JFactory.java:4547)
	at com.github.javabdd.JFactory.bdd_noderesize(JFactory.java:4533)
	at com.github.javabdd.JFactory.makenode(JFactory.java:4476)
	at com.github.javabdd.JFactory.bdd_makenode(JFactory.java:4414)
	at com.github.javabdd.JFactory.or_rec(JFactory.java:2254)
	at com.github.javabdd.JFactory.or_rec(JFactory.java:2253)
	at com.github.javabdd.JFactory.or_rec(JFactory.java:2252)
	at com.github.javabdd.JFactory.or_rec(JFactory.java:2252)
...

In doResize, the BDD node array is resized to a larger size, when needed. If it becomes too big, there is a signed integer overflow in computing the new size, and the size becomes negative, leading to a crash. Likely we'll need to fix this partly also in JavaBDD. JavaBDD should increase to Integer.MAX_VALUE. And the next time it should give some kind of out of memory error. CIF data-based synthesis should handle that correctly then.