search

loonwerks / jkind

JKind - An infinite-state model checker for safety properties in Lustre
http://loonwerks.com/tools/jkind.html
Other
52 stars 32 forks source link

Stack Overflow #27

Closed lgwagner closed 8 years ago

lgwagner commented 8 years ago

The attached file (renamed to a TXT file because Github will not accept a .lus extension) generates a stack overflow in JKind 2.2.1. It seems to be associated with the PDR process.

-------------------------------------
--^^--        SUMMARY          --^^--
-------------------------------------

VALID PROPERTIES: [high_turn_bound]

UNKNOWN PROPERTIES: [low_turn_bound]

pdr process failed java.lang.StackOverflowError at java.util.IdentityHashMap.hash(Unknown Source) at java.util.IdentityHashMap.put(Unknown Source) at de.uni_freiburg.informatik.ultimate.smtinterpol.util.IdentityHashSet.add(IdentityHashSet.java:51) at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.UnsatCoreCollector.accept(UnsatCoreCollector.java:58) at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.UnsatCoreCollector.visit(UnsatCoreCollector.java:70) at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.UnsatCoreCollector.accept(UnsatCoreCollector.java:62) at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.UnsatCoreCollector.visit(UnsatCoreCollector.java:70) at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.UnsatCoreCollector.accept(UnsatCoreCollector.java:62) at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.UnsatCoreCollector.visit(UnsatCoreCollector.java:70)

TicTacToe.spear.lus.txt

agacek commented 8 years ago

I've opened an issue for SMTInterpol. Hopefully they can fix the overflow. Otherwise we can just catch the overflow and kill that PDR thread. It's not ideal, but it's better than crashing.

https://github.com/ultimate-pa/smtinterpol/issues/9