./jayhorn -j tmp


--------------------------------------------------------------------------------


[root] - 		 ---   JAYHORN : Static Analayzer for Java Programs ---- 
[root] - 	 Verification : safety
[root] - 	 Solver : eldarica
[root] - Building CFG  ... 
Soot failed to parse <Main: void main(JayArray_java_lang_String)>
com.google.common.base.VerifyException
	at com.google.common.base.Verify.verify(Verify.java:98)
	at soottocfg.cfg.expression.TupleAccessExpression.<init>(TupleAccessExpression.java:35)
	at soottocfg.soot.util.SootTranslationHelpers.createInstanceOfExpression(SootTranslationHelpers.java:173)
	at soottocfg.soot.visitors.SootValueSwitch.caseInstanceOfExpr(SootValueSwitch.java:488)
	at soot.jimple.internal.AbstractInstanceOfExpr.apply(AbstractInstanceOfExpr.java:126)
	at soottocfg.soot.visitors.SootStmtSwitch.translateDefinitionStmt(SootStmtSwitch.java:689)
	at soottocfg.soot.visitors.SootStmtSwitch.caseAssignStmt(SootStmtSwitch.java:232)
	at soot.jimple.internal.JAssignStmt.apply(JAssignStmt.java:238)
	at soottocfg.soot.visitors.SootStmtSwitch.<init>(SootStmtSwitch.java:124)
	at soottocfg.soot.SootToCfg.constructCfg(SootToCfg.java:272)
	at soottocfg.soot.SootToCfg.constructCfg(SootToCfg.java:242)
	at soottocfg.soot.SootToCfg.constructCfg(SootToCfg.java:296)
	at soottocfg.soot.SootToCfg.run(SootToCfg.java:121)
	at jayhorn.Main.safetyAnalysis(Main.java:52)
	at jayhorn.Main.main(Main.java:100)
2018-07-29 03:01:57,479 ERROR (main) [root] - com.google.common.base.VerifyException
Exception in thread "main" com.google.common.base.VerifyException
	at com.google.common.base.Verify.verify(Verify.java:98)
	at soottocfg.cfg.expression.TupleAccessExpression.<init>(TupleAccessExpression.java:35)
	at soottocfg.soot.util.SootTranslationHelpers.createInstanceOfExpression(SootTranslationHelpers.java:173)
	at soottocfg.soot.visitors.SootValueSwitch.caseInstanceOfExpr(SootValueSwitch.java:488)
	at soot.jimple.internal.AbstractInstanceOfExpr.apply(AbstractInstanceOfExpr.java:126)
	at soottocfg.soot.visitors.SootStmtSwitch.translateDefinitionStmt(SootStmtSwitch.java:689)
	at soottocfg.soot.visitors.SootStmtSwitch.caseAssignStmt(SootStmtSwitch.java:232)
	at soot.jimple.internal.JAssignStmt.apply(JAssignStmt.java:238)
	at soottocfg.soot.visitors.SootStmtSwitch.<init>(SootStmtSwitch.java:124)
	at soottocfg.soot.SootToCfg.constructCfg(SootToCfg.java:272)
	at soottocfg.soot.SootToCfg.constructCfg(SootToCfg.java:242)
	at soottocfg.soot.SootToCfg.constructCfg(SootToCfg.java:296)
	at soottocfg.soot.SootToCfg.run(SootToCfg.java:121)
	at jayhorn.Main.safetyAnalysis(Main.java:52)
	at jayhorn.Main.main(Main.java:100)